H-Termination proof of /home/matraf/haskell/eval_FullyBlown

YES 16.492 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:

↳ HASKELL

  ↳ CR

mainModule List

((sort :: [Float] -> [Float]) :: [Float] -> [Float])

module List where

import qualified Maybe
import qualified Prelude

merge :: (a -> a -> Ordering) -> [a] -> [a] -> [a]

merge

cmp xs []

merge

cmp [] ys

merge

cmp (x : xs) (y : ys)

case	x `cmp` y of
	GT	->	y : merge cmp (x : xs) ys
	_	->	x : merge cmp xs (y : ys)

merge_pairs :: (a -> a -> Ordering) -> [[a]] -> [[a]]

merge_pairs	cmp []	=	[]
merge_pairs	cmp (xs : [])	=	xs : []
merge_pairs	cmp (xs : ys : xss)	=	merge cmp xs ys : merge_pairs cmp xss

mergesort :: (a -> a -> Ordering) -> [a] -> [a]

mergesort

cmp

mergesort' cmp . map wrap

mergesort' :: (a -> a -> Ordering) -> [[a]] -> [a]

mergesort'	cmp []	=	[]
mergesort'	cmp (xs : [])	=	xs
mergesort'	cmp xss	=	mergesort' cmp (merge_pairs cmp xss)

sort :: Ord a => [a] -> [a]

sort

mergesort compare l

wrap :: a -> [a]

wrap

x : []

module Maybe where

import qualified List
import qualified Prelude

Case Reductions:
The following Case expression

case cmp x y of
GT → y : merge cmp (x : xs) ys

_ → x : merge cmp xs (y : ys)

is transformed to

merge0 y cmp x xs ys GT = y : merge cmp (x : xs) ys

merge0 y cmp x xs ys _ = x : merge cmp xs (y : ys)

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

mainModule List

((sort :: [Float] -> [Float]) :: [Float] -> [Float])

module List where

import qualified Maybe
import qualified Prelude

merge :: (a -> a -> Ordering) -> [a] -> [a] -> [a]

merge	cmp xs []	=	xs
merge	cmp [] ys	=	ys
merge	cmp (x : xs) (y : ys)	=	merge0 y cmp x xs ys (x `cmp` y)

merge0	y cmp x xs ys GT	=	y : merge cmp (x : xs) ys
merge0	y cmp x xs ys _	=	x : merge cmp xs (y : ys)

merge_pairs :: (a -> a -> Ordering) -> [[a]] -> [[a]]

merge_pairs	cmp []	=	[]
merge_pairs	cmp (xs : [])	=	xs : []
merge_pairs	cmp (xs : ys : xss)	=	merge cmp xs ys : merge_pairs cmp xss

mergesort :: (a -> a -> Ordering) -> [a] -> [a]

mergesort

cmp

mergesort' cmp . map wrap

mergesort' :: (a -> a -> Ordering) -> [[a]] -> [a]

mergesort'	cmp []	=	[]
mergesort'	cmp (xs : [])	=	xs
mergesort'	cmp xss	=	mergesort' cmp (merge_pairs cmp xss)

sort :: Ord a => [a] -> [a]

sort

mergesort compare l

wrap :: a -> [a]

wrap

x : []

module Maybe where

import qualified List
import qualified Prelude

Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

mainModule List

((sort :: [Float] -> [Float]) :: [Float] -> [Float])

module List where

import qualified Maybe
import qualified Prelude

merge :: (a -> a -> Ordering) -> [a] -> [a] -> [a]

merge	cmp xs []	=	xs
merge	cmp [] ys	=	ys
merge	cmp (x : xs) (y : ys)	=	merge0 y cmp x xs ys (x `cmp` y)

merge0	y cmp x xs ys GT	=	y : merge cmp (x : xs) ys
merge0	y cmp x xs ys vw	=	x : merge cmp xs (y : ys)

merge_pairs :: (a -> a -> Ordering) -> [[a]] -> [[a]]

merge_pairs	cmp []	=	[]
merge_pairs	cmp (xs : [])	=	xs : []
merge_pairs	cmp (xs : ys : xss)	=	merge cmp xs ys : merge_pairs cmp xss

mergesort :: (a -> a -> Ordering) -> [a] -> [a]

mergesort

cmp

mergesort' cmp . map wrap

mergesort' :: (a -> a -> Ordering) -> [[a]] -> [a]

mergesort'	cmp []	=	[]
mergesort'	cmp (xs : [])	=	xs
mergesort'	cmp xss	=	mergesort' cmp (merge_pairs cmp xss)

sort :: Ord a => [a] -> [a]

sort

mergesort compare l

wrap :: a -> [a]

wrap

x : []

module Maybe where

import qualified List
import qualified Prelude

Cond Reductions:
The following Function with conditions

undefined

| False

= undefined

is transformed to

undefined = undefined1

undefined0 True = undefined

undefined1 = undefined0 False

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

mainModule List

(sort :: [Float] -> [Float])

module List where

import qualified Maybe
import qualified Prelude

merge :: (a -> a -> Ordering) -> [a] -> [a] -> [a]

merge	cmp xs []	=	xs
merge	cmp [] ys	=	ys
merge	cmp (x : xs) (y : ys)	=	merge0 y cmp x xs ys (x `cmp` y)

merge0	y cmp x xs ys GT	=	y : merge cmp (x : xs) ys
merge0	y cmp x xs ys vw	=	x : merge cmp xs (y : ys)

merge_pairs :: (a -> a -> Ordering) -> [[a]] -> [[a]]

merge_pairs	cmp []	=	[]
merge_pairs	cmp (xs : [])	=	xs : []
merge_pairs	cmp (xs : ys : xss)	=	merge cmp xs ys : merge_pairs cmp xss

mergesort :: (a -> a -> Ordering) -> [a] -> [a]

mergesort

cmp

mergesort' cmp . map wrap

mergesort' :: (a -> a -> Ordering) -> [[a]] -> [a]

mergesort'	cmp []	=	[]
mergesort'	cmp (xs : [])	=	xs
mergesort'	cmp xss	=	mergesort' cmp (merge_pairs cmp xss)

sort :: Ord a => [a] -> [a]

sort

mergesort compare l

wrap :: a -> [a]

wrap

x : []

module Maybe where

import qualified List
import qualified Prelude

Haskell To QDPs

digraph dp_graph {
node [outthreshold=100, inthreshold=100];1[label="sort",fontsize=16,color="grey",shape="box"];1 -> 3[label="",style="dashed", color="grey", weight=3];
3[label="sort vz3",fontsize=16,color="black",shape="triangle"];3 -> 4[label="",style="solid", color="black", weight=3];
4[label="mergesort compare vz3",fontsize=16,color="black",shape="box"];4 -> 5[label="",style="solid", color="black", weight=3];
5[label="(mergesort' compare) . map wrap",fontsize=16,color="black",shape="box"];5 -> 6[label="",style="solid", color="black", weight=3];
6[label="mergesort' compare (map wrap vz3)",fontsize=16,color="burlywood",shape="box"];8075[label="vz3/vz30 : vz31",fontsize=10,color="white",style="solid",shape="box"];6 -> 8075[label="",style="solid", color="burlywood", weight=9];
8075 -> 7[label="",style="solid", color="burlywood", weight=3];
8076[label="vz3/[]",fontsize=10,color="white",style="solid",shape="box"];6 -> 8076[label="",style="solid", color="burlywood", weight=9];
8076 -> 8[label="",style="solid", color="burlywood", weight=3];
7[label="mergesort' compare (map wrap (vz30 : vz31))",fontsize=16,color="black",shape="box"];7 -> 9[label="",style="solid", color="black", weight=3];
8[label="mergesort' compare (map wrap [])",fontsize=16,color="black",shape="box"];8 -> 10[label="",style="solid", color="black", weight=3];
9[label="mergesort' compare (wrap vz30 : map wrap vz31)",fontsize=16,color="burlywood",shape="box"];8077[label="vz31/vz310 : vz311",fontsize=10,color="white",style="solid",shape="box"];9 -> 8077[label="",style="solid", color="burlywood", weight=9];
8077 -> 11[label="",style="solid", color="burlywood", weight=3];
8078[label="vz31/[]",fontsize=10,color="white",style="solid",shape="box"];9 -> 8078[label="",style="solid", color="burlywood", weight=9];
8078 -> 12[label="",style="solid", color="burlywood", weight=3];
10[label="mergesort' compare []",fontsize=16,color="black",shape="box"];10 -> 13[label="",style="solid", color="black", weight=3];
11[label="mergesort' compare (wrap vz30 : map wrap (vz310 : vz311))",fontsize=16,color="black",shape="box"];11 -> 14[label="",style="solid", color="black", weight=3];
12[label="mergesort' compare (wrap vz30 : map wrap [])",fontsize=16,color="black",shape="box"];12 -> 15[label="",style="solid", color="black", weight=3];
13[label="[]",fontsize=16,color="green",shape="box"];14[label="mergesort' compare (wrap vz30 : wrap vz310 : map wrap vz311)",fontsize=16,color="black",shape="box"];14 -> 16[label="",style="solid", color="black", weight=3];
15[label="mergesort' compare (wrap vz30 : [])",fontsize=16,color="black",shape="box"];15 -> 17[label="",style="solid", color="black", weight=3];
16[label="mergesort' compare (merge_pairs compare (wrap vz30 : wrap vz310 : map wrap vz311))",fontsize=16,color="black",shape="box"];16 -> 18[label="",style="solid", color="black", weight=3];
17[label="wrap vz30",fontsize=16,color="black",shape="triangle"];17 -> 19[label="",style="solid", color="black", weight=3];
18 -> 7630[label="",style="dashed", color="red", weight=0];
18[label="mergesort' compare (merge compare (wrap vz30) (wrap vz310) : merge_pairs compare (map wrap vz311))",fontsize=16,color="magenta"];18 -> 7631[label="",style="dashed", color="magenta", weight=3];
18 -> 7632[label="",style="dashed", color="magenta", weight=3];
19[label="vz30 : []",fontsize=16,color="green",shape="box"];7631[label="map wrap vz311",fontsize=16,color="burlywood",shape="triangle"];8080[label="vz311/vz3110 : vz3111",fontsize=10,color="white",style="solid",shape="box"];7631 -> 8080[label="",style="solid", color="burlywood", weight=9];
8080 -> 7785[label="",style="solid", color="burlywood", weight=3];
8081[label="vz311/[]",fontsize=10,color="white",style="solid",shape="box"];7631 -> 8081[label="",style="solid", color="burlywood", weight=9];
8081 -> 7786[label="",style="solid", color="burlywood", weight=3];
7632 -> 7787[label="",style="dashed", color="red", weight=0];
7632[label="merge compare (wrap vz30) (wrap vz310)",fontsize=16,color="magenta"];7632 -> 7788[label="",style="dashed", color="magenta", weight=3];
7632 -> 7789[label="",style="dashed", color="magenta", weight=3];
7630[label="mergesort' compare (vz514 : merge_pairs compare vz515)\n  Ord a",fontsize=16,color="burlywood",shape="triangle"];8083[label="vz515/vz5150 : vz5151",fontsize=10,color="white",style="solid",shape="box"];7630 -> 8083[label="",style="solid", color="burlywood", weight=9];
8083 -> 7790[label="",style="solid", color="burlywood", weight=3];
8084[label="vz515/[]",fontsize=10,color="white",style="solid",shape="box"];7630 -> 8084[label="",style="solid", color="burlywood", weight=9];
8084 -> 7791[label="",style="solid", color="burlywood", weight=3];
7785[label="map wrap (vz3110 : vz3111)",fontsize=16,color="black",shape="box"];7785 -> 7792[label="",style="solid", color="black", weight=3];
7786[label="map wrap []",fontsize=16,color="black",shape="box"];7786 -> 7793[label="",style="solid", color="black", weight=3];
7788 -> 17[label="",style="dashed", color="red", weight=0];
7788[label="wrap vz30",fontsize=16,color="magenta"];7789 -> 17[label="",style="dashed", color="red", weight=0];
7789[label="wrap vz310",fontsize=16,color="magenta"];7789 -> 7794[label="",style="dashed", color="magenta", weight=3];
7787[label="merge compare vz517 vz516",fontsize=16,color="burlywood",shape="triangle"];8087[label="vz516/vz5160 : vz5161",fontsize=10,color="white",style="solid",shape="box"];7787 -> 8087[label="",style="solid", color="burlywood", weight=9];
8087 -> 7795[label="",style="solid", color="burlywood", weight=3];
8088[label="vz516/[]",fontsize=10,color="white",style="solid",shape="box"];7787 -> 8088[label="",style="solid", color="burlywood", weight=9];
8088 -> 7796[label="",style="solid", color="burlywood", weight=3];
7790[label="mergesort' compare (vz514 : merge_pairs compare (vz5150 : vz5151))\n  Ord a",fontsize=16,color="burlywood",shape="box"];8089[label="vz5151/vz51510 : vz51511",fontsize=10,color="white",style="solid",shape="box"];7790 -> 8089[label="",style="solid", color="burlywood", weight=9];
8089 -> 7797[label="",style="solid", color="burlywood", weight=3];
8090[label="vz5151/[]",fontsize=10,color="white",style="solid",shape="box"];7790 -> 8090[label="",style="solid", color="burlywood", weight=9];
8090 -> 7798[label="",style="solid", color="burlywood", weight=3];
7791[label="mergesort' compare (vz514 : merge_pairs compare [])\n  Ord a",fontsize=16,color="black",shape="box"];7791 -> 7799[label="",style="solid", color="black", weight=3];
7792[label="wrap vz3110 : map wrap vz3111",fontsize=16,color="green",shape="box"];7792 -> 7800[label="",style="dashed", color="green", weight=3];
7792 -> 7801[label="",style="dashed", color="green", weight=3];
7793[label="[]",fontsize=16,color="green",shape="box"];7794[label="vz310",fontsize=16,color="green",shape="box"];7795[label="merge compare vz517 (vz5160 : vz5161)",fontsize=16,color="burlywood",shape="box"];8091[label="vz517/vz5170 : vz5171",fontsize=10,color="white",style="solid",shape="box"];7795 -> 8091[label="",style="solid", color="burlywood", weight=9];
8091 -> 7802[label="",style="solid", color="burlywood", weight=3];
8092[label="vz517/[]",fontsize=10,color="white",style="solid",shape="box"];7795 -> 8092[label="",style="solid", color="burlywood", weight=9];
8092 -> 7803[label="",style="solid", color="burlywood", weight=3];
7796[label="merge compare vz517 []",fontsize=16,color="black",shape="box"];7796 -> 7804[label="",style="solid", color="black", weight=3];
7797[label="mergesort' compare (vz514 : merge_pairs compare (vz5150 : vz51510 : vz51511))\n  Ord a",fontsize=16,color="black",shape="box"];7797 -> 7805[label="",style="solid", color="black", weight=3];
7798[label="mergesort' compare (vz514 : merge_pairs compare (vz5150 : []))\n  Ord a",fontsize=16,color="black",shape="box"];7798 -> 7806[label="",style="solid", color="black", weight=3];
7799[label="mergesort' compare (vz514 : [])\n  Ord a",fontsize=16,color="black",shape="box"];7799 -> 7807[label="",style="solid", color="black", weight=3];
7800 -> 17[label="",style="dashed", color="red", weight=0];
7800[label="wrap vz3110",fontsize=16,color="magenta"];7800 -> 7808[label="",style="dashed", color="magenta", weight=3];
7801 -> 7631[label="",style="dashed", color="red", weight=0];
7801[label="map wrap vz3111",fontsize=16,color="magenta"];7801 -> 7809[label="",style="dashed", color="magenta", weight=3];
7802[label="merge compare (vz5170 : vz5171) (vz5160 : vz5161)",fontsize=16,color="black",shape="box"];7802 -> 7810[label="",style="solid", color="black", weight=3];
7803[label="merge compare [] (vz5160 : vz5161)",fontsize=16,color="black",shape="box"];7803 -> 7811[label="",style="solid", color="black", weight=3];
7804[label="vz517",fontsize=16,color="green",shape="box"];7805[label="mergesort' compare (vz514 : merge compare vz5150 vz51510 : merge_pairs compare vz51511)\n  Ord a",fontsize=16,color="black",shape="box"];7805 -> 7812[label="",style="solid", color="black", weight=3];
7806[label="mergesort' compare (vz514 : vz5150 : [])\n  Ord a",fontsize=16,color="black",shape="box"];7806 -> 7813[label="",style="solid", color="black", weight=3];
7807[label="vz514\n  Ord a",fontsize=16,color="green",shape="box"];7808[label="vz3110",fontsize=16,color="green",shape="box"];7809[label="vz3111",fontsize=16,color="green",shape="box"];7810 -> 7851[label="",style="dashed", color="red", weight=0];
7810[label="merge0 vz5160 compare vz5170 vz5171 vz5161 (compare vz5170 vz5160)",fontsize=16,color="magenta"];7810 -> 7852[label="",style="dashed", color="magenta", weight=3];
7810 -> 7853[label="",style="dashed", color="magenta", weight=3];
7810 -> 7854[label="",style="dashed", color="magenta", weight=3];
7810 -> 7855[label="",style="dashed", color="magenta", weight=3];
7810 -> 7856[label="",style="dashed", color="magenta", weight=3];
7811[label="vz5160 : vz5161",fontsize=16,color="green",shape="box"];7812[label="mergesort' compare (merge_pairs compare (vz514 : merge compare vz5150 vz51510 : merge_pairs compare vz51511))\n  Ord a",fontsize=16,color="black",shape="box"];7812 -> 7815[label="",style="solid", color="black", weight=3];
7813[label="mergesort' compare (merge_pairs compare (vz514 : vz5150 : []))\n  Ord a",fontsize=16,color="black",shape="box"];7813 -> 7816[label="",style="solid", color="black", weight=3];
7852[label="vz5161",fontsize=16,color="green",shape="box"];7853[label="compare vz5170 vz5160",fontsize=16,color="black",shape="triangle"];7853 -> 7867[label="",style="solid", color="black", weight=3];
7854[label="vz5170",fontsize=16,color="green",shape="box"];7855[label="vz5160",fontsize=16,color="green",shape="box"];7856[label="vz5171",fontsize=16,color="green",shape="box"];7851[label="merge0 vz524 compare vz525 vz526 vz527 vz528\n  Ord a",fontsize=16,color="burlywood",shape="triangle"];8096[label="vz528/LT",fontsize=10,color="white",style="solid",shape="box"];7851 -> 8096[label="",style="solid", color="burlywood", weight=9];
8096 -> 7868[label="",style="solid", color="burlywood", weight=3];
8097[label="vz528/EQ",fontsize=10,color="white",style="solid",shape="box"];7851 -> 8097[label="",style="solid", color="burlywood", weight=9];
8097 -> 7869[label="",style="solid", color="burlywood", weight=3];
8098[label="vz528/GT",fontsize=10,color="white",style="solid",shape="box"];7851 -> 8098[label="",style="solid", color="burlywood", weight=9];
8098 -> 7870[label="",style="solid", color="burlywood", weight=3];
7815 -> 7630[label="",style="dashed", color="red", weight=0];
7815[label="mergesort' compare (merge compare vz514 (merge compare vz5150 vz51510) : merge_pairs compare (merge_pairs compare vz51511))\n  Ord a",fontsize=16,color="magenta"];7815 -> 7818[label="",style="dashed", color="magenta", weight=3];
7815 -> 7819[label="",style="dashed", color="magenta", weight=3];
7816 -> 7630[label="",style="dashed", color="red", weight=0];
7816[label="mergesort' compare (merge compare vz514 vz5150 : merge_pairs compare [])\n  Ord a",fontsize=16,color="magenta"];7816 -> 7820[label="",style="dashed", color="magenta", weight=3];
7816 -> 7821[label="",style="dashed", color="magenta", weight=3];
7867[label="primCmpFloat vz5170 vz5160",fontsize=16,color="burlywood",shape="box"];8101[label="vz5170/Float vz51700 vz51701",fontsize=10,color="white",style="solid",shape="box"];7867 -> 8101[label="",style="solid", color="burlywood", weight=9];
8101 -> 7902[label="",style="solid", color="burlywood", weight=3];
7868[label="merge0 vz524 compare vz525 vz526 vz527 LT\n  Ord a",fontsize=16,color="black",shape="box"];7868 -> 7903[label="",style="solid", color="black", weight=3];
7869[label="merge0 vz524 compare vz525 vz526 vz527 EQ\n  Ord a",fontsize=16,color="black",shape="box"];7869 -> 7904[label="",style="solid", color="black", weight=3];
7870[label="merge0 vz524 compare vz525 vz526 vz527 GT\n  Ord a",fontsize=16,color="black",shape="box"];7870 -> 7905[label="",style="solid", color="black", weight=3];
7818[label="merge_pairs compare vz51511\n  Ord a",fontsize=16,color="burlywood",shape="triangle"];8102[label="vz51511/vz515110 : vz515111",fontsize=10,color="white",style="solid",shape="box"];7818 -> 8102[label="",style="solid", color="burlywood", weight=9];
8102 -> 7823[label="",style="solid", color="burlywood", weight=3];
8103[label="vz51511/[]",fontsize=10,color="white",style="solid",shape="box"];7818 -> 8103[label="",style="solid", color="burlywood", weight=9];
8103 -> 7824[label="",style="solid", color="burlywood", weight=3];
7819[label="merge compare vz514 (merge compare vz5150 vz51510)\n  Ord a",fontsize=16,color="burlywood",shape="box"];8104[label="vz51510/vz515100 : vz515101",fontsize=10,color="white",style="solid",shape="box"];7819 -> 8104[label="",style="solid", color="burlywood", weight=9];
8104 -> 7825[label="",style="solid", color="burlywood", weight=3];
8105[label="vz51510/[]",fontsize=10,color="white",style="solid",shape="box"];7819 -> 8105[label="",style="solid", color="burlywood", weight=9];
8105 -> 7826[label="",style="solid", color="burlywood", weight=3];
7820[label="[]\n  Ord a",fontsize=16,color="green",shape="box"];7821[label="merge compare vz514 vz5150\n  Ord a",fontsize=16,color="burlywood",shape="triangle"];8106[label="vz5150/vz51500 : vz51501",fontsize=10,color="white",style="solid",shape="box"];7821 -> 8106[label="",style="solid", color="burlywood", weight=9];
8106 -> 7827[label="",style="solid", color="burlywood", weight=3];
8107[label="vz5150/[]",fontsize=10,color="white",style="solid",shape="box"];7821 -> 8107[label="",style="solid", color="burlywood", weight=9];
8107 -> 7828[label="",style="solid", color="burlywood", weight=3];
7902[label="primCmpFloat (Float vz51700 vz51701) vz5160",fontsize=16,color="burlywood",shape="box"];8108[label="vz5160/Float vz51600 vz51601",fontsize=10,color="white",style="solid",shape="box"];7902 -> 8108[label="",style="solid", color="burlywood", weight=9];
8108 -> 7949[label="",style="solid", color="burlywood", weight=3];
7903[label="vz525 : merge compare vz526 (vz524 : vz527)\n  Ord a",fontsize=16,color="green",shape="box"];7903 -> 7950[label="",style="dashed", color="green", weight=3];
7904[label="vz525 : merge compare vz526 (vz524 : vz527)\n  Ord a",fontsize=16,color="green",shape="box"];7904 -> 7951[label="",style="dashed", color="green", weight=3];
7905[label="vz524 : merge compare (vz525 : vz526) vz527\n  Ord a",fontsize=16,color="green",shape="box"];7905 -> 7952[label="",style="dashed", color="green", weight=3];
7823[label="merge_pairs compare (vz515110 : vz515111)\n  Ord a",fontsize=16,color="burlywood",shape="box"];8109[label="vz515111/vz5151110 : vz5151111",fontsize=10,color="white",style="solid",shape="box"];7823 -> 8109[label="",style="solid", color="burlywood", weight=9];
8109 -> 7830[label="",style="solid", color="burlywood", weight=3];
8110[label="vz515111/[]",fontsize=10,color="white",style="solid",shape="box"];7823 -> 8110[label="",style="solid", color="burlywood", weight=9];
8110 -> 7831[label="",style="solid", color="burlywood", weight=3];
7824[label="merge_pairs compare []\n  Ord a",fontsize=16,color="black",shape="box"];7824 -> 7832[label="",style="solid", color="black", weight=3];
7825[label="merge compare vz514 (merge compare vz5150 (vz515100 : vz515101))\n  Ord a",fontsize=16,color="burlywood",shape="box"];8111[label="vz5150/vz51500 : vz51501",fontsize=10,color="white",style="solid",shape="box"];7825 -> 8111[label="",style="solid", color="burlywood", weight=9];
8111 -> 7833[label="",style="solid", color="burlywood", weight=3];
8112[label="vz5150/[]",fontsize=10,color="white",style="solid",shape="box"];7825 -> 8112[label="",style="solid", color="burlywood", weight=9];
8112 -> 7834[label="",style="solid", color="burlywood", weight=3];
7826[label="merge compare vz514 (merge compare vz5150 [])\n  Ord a",fontsize=16,color="black",shape="box"];7826 -> 7835[label="",style="solid", color="black", weight=3];
7827[label="merge compare vz514 (vz51500 : vz51501)\n  Ord a",fontsize=16,color="burlywood",shape="box"];8113[label="vz514/vz5140 : vz5141",fontsize=10,color="white",style="solid",shape="box"];7827 -> 8113[label="",style="solid", color="burlywood", weight=9];
8113 -> 7836[label="",style="solid", color="burlywood", weight=3];
8114[label="vz514/[]",fontsize=10,color="white",style="solid",shape="box"];7827 -> 8114[label="",style="solid", color="burlywood", weight=9];
8114 -> 7837[label="",style="solid", color="burlywood", weight=3];
7828[label="merge compare vz514 []\n  Ord a",fontsize=16,color="black",shape="box"];7828 -> 7838[label="",style="solid", color="black", weight=3];
7949[label="primCmpFloat (Float vz51700 vz51701) (Float vz51600 vz51601)",fontsize=16,color="black",shape="box"];7949 -> 7955[label="",style="solid", color="black", weight=3];
7950 -> 7821[label="",style="dashed", color="red", weight=0];
7950[label="merge compare vz526 (vz524 : vz527)\n  Ord a",fontsize=16,color="magenta"];7950 -> 7956[label="",style="dashed", color="magenta", weight=3];
7950 -> 7957[label="",style="dashed", color="magenta", weight=3];
7951 -> 7821[label="",style="dashed", color="red", weight=0];
7951[label="merge compare vz526 (vz524 : vz527)\n  Ord a",fontsize=16,color="magenta"];7951 -> 7958[label="",style="dashed", color="magenta", weight=3];
7951 -> 7959[label="",style="dashed", color="magenta", weight=3];
7952 -> 7821[label="",style="dashed", color="red", weight=0];
7952[label="merge compare (vz525 : vz526) vz527\n  Ord a",fontsize=16,color="magenta"];7952 -> 7960[label="",style="dashed", color="magenta", weight=3];
7952 -> 7961[label="",style="dashed", color="magenta", weight=3];
7830[label="merge_pairs compare (vz515110 : vz5151110 : vz5151111)\n  Ord a",fontsize=16,color="black",shape="box"];7830 -> 7840[label="",style="solid", color="black", weight=3];
7831[label="merge_pairs compare (vz515110 : [])\n  Ord a",fontsize=16,color="black",shape="box"];7831 -> 7841[label="",style="solid", color="black", weight=3];
7832[label="[]\n  Ord a",fontsize=16,color="green",shape="box"];7833[label="merge compare vz514 (merge compare (vz51500 : vz51501) (vz515100 : vz515101))\n  Ord a",fontsize=16,color="black",shape="box"];7833 -> 7842[label="",style="solid", color="black", weight=3];
7834[label="merge compare vz514 (merge compare [] (vz515100 : vz515101))\n  Ord a",fontsize=16,color="black",shape="box"];7834 -> 7843[label="",style="solid", color="black", weight=3];
7835 -> 7821[label="",style="dashed", color="red", weight=0];
7835[label="merge compare vz514 vz5150\n  Ord a",fontsize=16,color="magenta"];7836[label="merge compare (vz5140 : vz5141) (vz51500 : vz51501)\n  Ord a",fontsize=16,color="black",shape="box"];7836 -> 7844[label="",style="solid", color="black", weight=3];
7837[label="merge compare [] (vz51500 : vz51501)\n  Ord a",fontsize=16,color="black",shape="box"];7837 -> 7845[label="",style="solid", color="black", weight=3];
7838[label="vz514\n  Ord a",fontsize=16,color="green",shape="box"];7955 -> 7883[label="",style="dashed", color="red", weight=0];
7955[label="compare (vz51700 * vz51600) (vz51701 * vz51601)",fontsize=16,color="magenta"];7955 -> 7966[label="",style="dashed", color="magenta", weight=3];
7955 -> 7967[label="",style="dashed", color="magenta", weight=3];
7956[label="vz526\n  Ord a",fontsize=16,color="green",shape="box"];7957[label="vz524 : vz527\n  Ord a",fontsize=16,color="green",shape="box"];7958[label="vz526\n  Ord a",fontsize=16,color="green",shape="box"];7959[label="vz524 : vz527\n  Ord a",fontsize=16,color="green",shape="box"];7960[label="vz525 : vz526\n  Ord a",fontsize=16,color="green",shape="box"];7961[label="vz527\n  Ord a",fontsize=16,color="green",shape="box"];7840[label="merge compare vz515110 vz5151110 : merge_pairs compare vz5151111\n  Ord a",fontsize=16,color="green",shape="box"];7840 -> 7847[label="",style="dashed", color="green", weight=3];
7840 -> 7848[label="",style="dashed", color="green", weight=3];
7841[label="vz515110 : []\n  Ord a",fontsize=16,color="green",shape="box"];7842 -> 7821[label="",style="dashed", color="red", weight=0];
7842[label="merge compare vz514 (merge0 vz515100 compare vz51500 vz51501 vz515101 (compare vz51500 vz515100))\n  Ord a",fontsize=16,color="magenta"];7842 -> 7849[label="",style="dashed", color="magenta", weight=3];
7843 -> 7821[label="",style="dashed", color="red", weight=0];
7843[label="merge compare vz514 (vz515100 : vz515101)\n  Ord a",fontsize=16,color="magenta"];7843 -> 7850[label="",style="dashed", color="magenta", weight=3];
7844 -> 7851[label="",style="dashed", color="red", weight=0];
7844[label="merge0 vz51500 compare vz5140 vz5141 vz51501 (compare vz5140 vz51500)\n  Ord a",fontsize=16,color="magenta"];7844 -> 7857[label="",style="dashed", color="magenta", weight=3];
7844 -> 7858[label="",style="dashed", color="magenta", weight=3];
7844 -> 7859[label="",style="dashed", color="magenta", weight=3];
7844 -> 7860[label="",style="dashed", color="magenta", weight=3];
7844 -> 7861[label="",style="dashed", color="magenta", weight=3];
7845[label="vz51500 : vz51501\n  Ord a",fontsize=16,color="green",shape="box"];7966[label="vz51701 * vz51601",fontsize=16,color="black",shape="triangle"];7966 -> 7976[label="",style="solid", color="black", weight=3];
7967 -> 7966[label="",style="dashed", color="red", weight=0];
7967[label="vz51700 * vz51600",fontsize=16,color="magenta"];7967 -> 7977[label="",style="dashed", color="magenta", weight=3];
7967 -> 7978[label="",style="dashed", color="magenta", weight=3];
7883[label="compare vz5140 vz51500",fontsize=16,color="black",shape="triangle"];7883 -> 7916[label="",style="solid", color="black", weight=3];
7847 -> 7821[label="",style="dashed", color="red", weight=0];
7847[label="merge compare vz515110 vz5151110\n  Ord a",fontsize=16,color="magenta"];7847 -> 7871[label="",style="dashed", color="magenta", weight=3];
7847 -> 7872[label="",style="dashed", color="magenta", weight=3];
7848 -> 7818[label="",style="dashed", color="red", weight=0];
7848[label="merge_pairs compare vz5151111\n  Ord a",fontsize=16,color="magenta"];7848 -> 7873[label="",style="dashed", color="magenta", weight=3];
7849 -> 7851[label="",style="dashed", color="red", weight=0];
7849[label="merge0 vz515100 compare vz51500 vz51501 vz515101 (compare vz51500 vz515100)\n  Ord a",fontsize=16,color="magenta"];7849 -> 7862[label="",style="dashed", color="magenta", weight=3];
7849 -> 7863[label="",style="dashed", color="magenta", weight=3];
7849 -> 7864[label="",style="dashed", color="magenta", weight=3];
7849 -> 7865[label="",style="dashed", color="magenta", weight=3];
7849 -> 7866[label="",style="dashed", color="magenta", weight=3];
7850[label="vz515100 : vz515101\n  Ord a",fontsize=16,color="green",shape="box"];7857[label="vz51501\n  Ord a",fontsize=16,color="green",shape="box"];7858[label="compare vz5140 vz51500\n  Ord a",fontsize=16,color="blue",shape="box"];8127[label="compare :: (Maybe a) -> (Maybe a) -> Ordering",fontsize=10,color="white",style="solid",shape="box"];7858 -> 8127[label="",style="solid", color="blue", weight=9];
8127 -> 7874[label="",style="solid", color="blue", weight=3];
8128[label="compare :: Integer -> Integer -> Ordering",fontsize=10,color="white",style="solid",shape="box"];7858 -> 8128[label="",style="solid", color="blue", weight=9];
8128 -> 7875[label="",style="solid", color="blue", weight=3];
8129[label="compare :: Bool -> Bool -> Ordering",fontsize=10,color="white",style="solid",shape="box"];7858 -> 8129[label="",style="solid", color="blue", weight=9];
8129 -> 7876[label="",style="solid", color="blue", weight=3];
8130[label="compare :: Char -> Char -> Ordering",fontsize=10,color="white",style="solid",shape="box"];7858 -> 8130[label="",style="solid", color="blue", weight=9];
8130 -> 7877[label="",style="solid", color="blue", weight=3];
8131[label="compare :: ((@3) a b c) -> ((@3) a b c) -> Ordering",fontsize=10,color="white",style="solid",shape="box"];7858 -> 8131[label="",style="solid", color="blue", weight=9];
8131 -> 7878[label="",style="solid", color="blue", weight=3];
8132[label="compare :: Ordering -> Ordering -> Ordering",fontsize=10,color="white",style="solid",shape="box"];7858 -> 8132[label="",style="solid", color="blue", weight=9];
8132 -> 7879[label="",style="solid", color="blue", weight=3];
8133[label="compare :: ([] a) -> ([] a) -> Ordering",fontsize=10,color="white",style="solid",shape="box"];7858 -> 8133[label="",style="solid", color="blue", weight=9];
8133 -> 7880[label="",style="solid", color="blue", weight=3];
8134[label="compare :: Double -> Double -> Ordering",fontsize=10,color="white",style="solid",shape="box"];7858 -> 8134[label="",style="solid", color="blue", weight=9];
8134 -> 7881[label="",style="solid", color="blue", weight=3];
8135[label="compare :: Float -> Float -> Ordering",fontsize=10,color="white",style="solid",shape="box"];7858 -> 8135[label="",style="solid", color="blue", weight=9];
8135 -> 7882[label="",style="solid", color="blue", weight=3];
8136[label="compare :: Int -> Int -> Ordering",fontsize=10,color="white",style="solid",shape="box"];7858 -> 8136[label="",style="solid", color="blue", weight=9];
8136 -> 7883[label="",style="solid", color="blue", weight=3];
8137[label="compare :: (Either a b) -> (Either a b) -> Ordering",fontsize=10,color="white",style="solid",shape="box"];7858 -> 8137[label="",style="solid", color="blue", weight=9];
8137 -> 7884[label="",style="solid", color="blue", weight=3];
8138[label="compare :: () -> () -> Ordering",fontsize=10,color="white",style="solid",shape="box"];7858 -> 8138[label="",style="solid", color="blue", weight=9];
8138 -> 7885[label="",style="solid", color="blue", weight=3];
8139[label="compare :: ((@2) a b) -> ((@2) a b) -> Ordering",fontsize=10,color="white",style="solid",shape="box"];7858 -> 8139[label="",style="solid", color="blue", weight=9];
8139 -> 7886[label="",style="solid", color="blue", weight=3];
8140[label="compare :: (Ratio a) -> (Ratio a) -> Ordering",fontsize=10,color="white",style="solid",shape="box"];7858 -> 8140[label="",style="solid", color="blue", weight=9];
8140 -> 7887[label="",style="solid", color="blue", weight=3];
7859[label="vz5140\n  Ord a",fontsize=16,color="green",shape="box"];7860[label="vz51500\n  Ord a",fontsize=16,color="green",shape="box"];7861[label="vz5141\n  Ord a",fontsize=16,color="green",shape="box"];7976[label="primMulInt vz51701 vz51601",fontsize=16,color="burlywood",shape="box"];8141[label="vz51701/Pos vz517010",fontsize=10,color="white",style="solid",shape="box"];7976 -> 8141[label="",style="solid", color="burlywood", weight=9];
8141 -> 7991[label="",style="solid", color="burlywood", weight=3];
8142[label="vz51701/Neg vz517010",fontsize=10,color="white",style="solid",shape="box"];7976 -> 8142[label="",style="solid", color="burlywood", weight=9];
8142 -> 7992[label="",style="solid", color="burlywood", weight=3];
7977[label="vz51700",fontsize=16,color="green",shape="box"];7978[label="vz51600",fontsize=16,color="green",shape="box"];7916[label="primCmpInt vz5140 vz51500",fontsize=16,color="burlywood",shape="box"];8143[label="vz5140/Pos vz51400",fontsize=10,color="white",style="solid",shape="box"];7916 -> 8143[label="",style="solid", color="burlywood", weight=9];
8143 -> 7953[label="",style="solid", color="burlywood", weight=3];
8144[label="vz5140/Neg vz51400",fontsize=10,color="white",style="solid",shape="box"];7916 -> 8144[label="",style="solid", color="burlywood", weight=9];
8144 -> 7954[label="",style="solid", color="burlywood", weight=3];
7871[label="vz515110\n  Ord a",fontsize=16,color="green",shape="box"];7872[label="vz5151110\n  Ord a",fontsize=16,color="green",shape="box"];7873[label="vz5151111\n  Ord a",fontsize=16,color="green",shape="box"];7862[label="vz515101\n  Ord a",fontsize=16,color="green",shape="box"];7863[label="compare vz51500 vz515100\n  Ord a",fontsize=16,color="blue",shape="box"];8145[label="compare :: (Maybe a) -> (Maybe a) -> Ordering",fontsize=10,color="white",style="solid",shape="box"];7863 -> 8145[label="",style="solid", color="blue", weight=9];
8145 -> 7888[label="",style="solid", color="blue", weight=3];
8146[label="compare :: Integer -> Integer -> Ordering",fontsize=10,color="white",style="solid",shape="box"];7863 -> 8146[label="",style="solid", color="blue", weight=9];
8146 -> 7889[label="",style="solid", color="blue", weight=3];
8147[label="compare :: Bool -> Bool -> Ordering",fontsize=10,color="white",style="solid",shape="box"];7863 -> 8147[label="",style="solid", color="blue", weight=9];
8147 -> 7890[label="",style="solid", color="blue", weight=3];
8148[label="compare :: Char -> Char -> Ordering",fontsize=10,color="white",style="solid",shape="box"];7863 -> 8148[label="",style="solid", color="blue", weight=9];
8148 -> 7891[label="",style="solid", color="blue", weight=3];
8149[label="compare :: ((@3) a b c) -> ((@3) a b c) -> Ordering",fontsize=10,color="white",style="solid",shape="box"];7863 -> 8149[label="",style="solid", color="blue", weight=9];
8149 -> 7892[label="",style="solid", color="blue", weight=3];
8150[label="compare :: Ordering -> Ordering -> Ordering",fontsize=10,color="white",style="solid",shape="box"];7863 -> 8150[label="",style="solid", color="blue", weight=9];
8150 -> 7893[label="",style="solid", color="blue", weight=3];
8151[label="compare :: ([] a) -> ([] a) -> Ordering",fontsize=10,color="white",style="solid",shape="box"];7863 -> 8151[label="",style="solid", color="blue", weight=9];
8151 -> 7894[label="",style="solid", color="blue", weight=3];
8152[label="compare :: Double -> Double -> Ordering",fontsize=10,color="white",style="solid",shape="box"];7863 -> 8152[label="",style="solid", color="blue", weight=9];
8152 -> 7895[label="",style="solid", color="blue", weight=3];
8153[label="compare :: Float -> Float -> Ordering",fontsize=10,color="white",style="solid",shape="box"];7863 -> 8153[label="",style="solid", color="blue", weight=9];
8153 -> 7896[label="",style="solid", color="blue", weight=3];
8154[label="compare :: Int -> Int -> Ordering",fontsize=10,color="white",style="solid",shape="box"];7863 -> 8154[label="",style="solid", color="blue", weight=9];
8154 -> 7897[label="",style="solid", color="blue", weight=3];
8155[label="compare :: (Either a b) -> (Either a b) -> Ordering",fontsize=10,color="white",style="solid",shape="box"];7863 -> 8155[label="",style="solid", color="blue", weight=9];
8155 -> 7898[label="",style="solid", color="blue", weight=3];
8156[label="compare :: () -> () -> Ordering",fontsize=10,color="white",style="solid",shape="box"];7863 -> 8156[label="",style="solid", color="blue", weight=9];
8156 -> 7899[label="",style="solid", color="blue", weight=3];
8157[label="compare :: ((@2) a b) -> ((@2) a b) -> Ordering",fontsize=10,color="white",style="solid",shape="box"];7863 -> 8157[label="",style="solid", color="blue", weight=9];
8157 -> 7900[label="",style="solid", color="blue", weight=3];
8158[label="compare :: (Ratio a) -> (Ratio a) -> Ordering",fontsize=10,color="white",style="solid",shape="box"];7863 -> 8158[label="",style="solid", color="blue", weight=9];
8158 -> 7901[label="",style="solid", color="blue", weight=3];
7864[label="vz51500\n  Ord a",fontsize=16,color="green",shape="box"];7865[label="vz515100\n  Ord a",fontsize=16,color="green",shape="box"];7866[label="vz51501\n  Ord a",fontsize=16,color="green",shape="box"];7874[label="compare vz5140 vz51500\n  Ord a",fontsize=16,color="black",shape="triangle"];7874 -> 7906[label="",style="solid", color="black", weight=3];
7875[label="compare vz5140 vz51500",fontsize=16,color="black",shape="triangle"];7875 -> 7907[label="",style="solid", color="black", weight=3];
7876[label="compare vz5140 vz51500",fontsize=16,color="black",shape="triangle"];7876 -> 7908[label="",style="solid", color="black", weight=3];
7877[label="compare vz5140 vz51500",fontsize=16,color="black",shape="triangle"];7877 -> 7909[label="",style="solid", color="black", weight=3];
7878[label="compare vz5140 vz51500\n  Ord a  Ord b  Ord c",fontsize=16,color="black",shape="triangle"];7878 -> 7910[label="",style="solid", color="black", weight=3];
7879[label="compare vz5140 vz51500",fontsize=16,color="black",shape="triangle"];7879 -> 7911[label="",style="solid", color="black", weight=3];
7880[label="compare vz5140 vz51500\n  Ord a",fontsize=16,color="black",shape="triangle"];7880 -> 7912[label="",style="solid", color="black", weight=3];
7881[label="compare vz5140 vz51500",fontsize=16,color="black",shape="triangle"];7881 -> 7913[label="",style="solid", color="black", weight=3];
7882 -> 7853[label="",style="dashed", color="red", weight=0];
7882[label="compare vz5140 vz51500",fontsize=16,color="magenta"];7882 -> 7914[label="",style="dashed", color="magenta", weight=3];
7882 -> 7915[label="",style="dashed", color="magenta", weight=3];
7884[label="compare vz5140 vz51500\n  Ord a  Ord b",fontsize=16,color="black",shape="triangle"];7884 -> 7917[label="",style="solid", color="black", weight=3];
7885[label="compare vz5140 vz51500",fontsize=16,color="black",shape="triangle"];7885 -> 7918[label="",style="solid", color="black", weight=3];
7886[label="compare vz5140 vz51500\n  Ord a  Ord b",fontsize=16,color="black",shape="triangle"];7886 -> 7919[label="",style="solid", color="black", weight=3];
7887[label="compare vz5140 vz51500\n  Integral a",fontsize=16,color="black",shape="triangle"];7887 -> 7920[label="",style="solid", color="black", weight=3];
7991[label="primMulInt (Pos vz517010) vz51601",fontsize=16,color="burlywood",shape="box"];8160[label="vz51601/Pos vz516010",fontsize=10,color="white",style="solid",shape="box"];7991 -> 8160[label="",style="solid", color="burlywood", weight=9];
8160 -> 8005[label="",style="solid", color="burlywood", weight=3];
8161[label="vz51601/Neg vz516010",fontsize=10,color="white",style="solid",shape="box"];7991 -> 8161[label="",style="solid", color="burlywood", weight=9];
8161 -> 8006[label="",style="solid", color="burlywood", weight=3];
7992[label="primMulInt (Neg vz517010) vz51601",fontsize=16,color="burlywood",shape="box"];8162[label="vz51601/Pos vz516010",fontsize=10,color="white",style="solid",shape="box"];7992 -> 8162[label="",style="solid", color="burlywood", weight=9];
8162 -> 8007[label="",style="solid", color="burlywood", weight=3];
8163[label="vz51601/Neg vz516010",fontsize=10,color="white",style="solid",shape="box"];7992 -> 8163[label="",style="solid", color="burlywood", weight=9];
8163 -> 8008[label="",style="solid", color="burlywood", weight=3];
7953[label="primCmpInt (Pos vz51400) vz51500",fontsize=16,color="burlywood",shape="box"];8164[label="vz51400/Succ vz514000",fontsize=10,color="white",style="solid",shape="box"];7953 -> 8164[label="",style="solid", color="burlywood", weight=9];
8164 -> 7962[label="",style="solid", color="burlywood", weight=3];
8165[label="vz51400/Zero",fontsize=10,color="white",style="solid",shape="box"];7953 -> 8165[label="",style="solid", color="burlywood", weight=9];
8165 -> 7963[label="",style="solid", color="burlywood", weight=3];
7954[label="primCmpInt (Neg vz51400) vz51500",fontsize=16,color="burlywood",shape="box"];8166[label="vz51400/Succ vz514000",fontsize=10,color="white",style="solid",shape="box"];7954 -> 8166[label="",style="solid", color="burlywood", weight=9];
8166 -> 7964[label="",style="solid", color="burlywood", weight=3];
8167[label="vz51400/Zero",fontsize=10,color="white",style="solid",shape="box"];7954 -> 8167[label="",style="solid", color="burlywood", weight=9];
8167 -> 7965[label="",style="solid", color="burlywood", weight=3];
7888 -> 7874[label="",style="dashed", color="red", weight=0];
7888[label="compare vz51500 vz515100\n  Ord a",fontsize=16,color="magenta"];7888 -> 7921[label="",style="dashed", color="magenta", weight=3];
7888 -> 7922[label="",style="dashed", color="magenta", weight=3];
7889 -> 7875[label="",style="dashed", color="red", weight=0];
7889[label="compare vz51500 vz515100",fontsize=16,color="magenta"];7889 -> 7923[label="",style="dashed", color="magenta", weight=3];
7889 -> 7924[label="",style="dashed", color="magenta", weight=3];
7890 -> 7876[label="",style="dashed", color="red", weight=0];
7890[label="compare vz51500 vz515100",fontsize=16,color="magenta"];7890 -> 7925[label="",style="dashed", color="magenta", weight=3];
7890 -> 7926[label="",style="dashed", color="magenta", weight=3];
7891 -> 7877[label="",style="dashed", color="red", weight=0];
7891[label="compare vz51500 vz515100",fontsize=16,color="magenta"];7891 -> 7927[label="",style="dashed", color="magenta", weight=3];
7891 -> 7928[label="",style="dashed", color="magenta", weight=3];
7892 -> 7878[label="",style="dashed", color="red", weight=0];
7892[label="compare vz51500 vz515100\n  Ord a  Ord b  Ord c",fontsize=16,color="magenta"];7892 -> 7929[label="",style="dashed", color="magenta", weight=3];
7892 -> 7930[label="",style="dashed", color="magenta", weight=3];
7893 -> 7879[label="",style="dashed", color="red", weight=0];
7893[label="compare vz51500 vz515100",fontsize=16,color="magenta"];7893 -> 7931[label="",style="dashed", color="magenta", weight=3];
7893 -> 7932[label="",style="dashed", color="magenta", weight=3];
7894 -> 7880[label="",style="dashed", color="red", weight=0];
7894[label="compare vz51500 vz515100\n  Ord a",fontsize=16,color="magenta"];7894 -> 7933[label="",style="dashed", color="magenta", weight=3];
7894 -> 7934[label="",style="dashed", color="magenta", weight=3];
7895 -> 7881[label="",style="dashed", color="red", weight=0];
7895[label="compare vz51500 vz515100",fontsize=16,color="magenta"];7895 -> 7935[label="",style="dashed", color="magenta", weight=3];
7895 -> 7936[label="",style="dashed", color="magenta", weight=3];
7896 -> 7853[label="",style="dashed", color="red", weight=0];
7896[label="compare vz51500 vz515100",fontsize=16,color="magenta"];7896 -> 7937[label="",style="dashed", color="magenta", weight=3];
7896 -> 7938[label="",style="dashed", color="magenta", weight=3];
7897 -> 7883[label="",style="dashed", color="red", weight=0];
7897[label="compare vz51500 vz515100",fontsize=16,color="magenta"];7897 -> 7939[label="",style="dashed", color="magenta", weight=3];
7897 -> 7940[label="",style="dashed", color="magenta", weight=3];
7898 -> 7884[label="",style="dashed", color="red", weight=0];
7898[label="compare vz51500 vz515100\n  Ord a  Ord b",fontsize=16,color="magenta"];7898 -> 7941[label="",style="dashed", color="magenta", weight=3];
7898 -> 7942[label="",style="dashed", color="magenta", weight=3];
7899 -> 7885[label="",style="dashed", color="red", weight=0];
7899[label="compare vz51500 vz515100",fontsize=16,color="magenta"];7899 -> 7943[label="",style="dashed", color="magenta", weight=3];
7899 -> 7944[label="",style="dashed", color="magenta", weight=3];
7900 -> 7886[label="",style="dashed", color="red", weight=0];
7900[label="compare vz51500 vz515100\n  Ord a  Ord b",fontsize=16,color="magenta"];7900 -> 7945[label="",style="dashed", color="magenta", weight=3];
7900 -> 7946[label="",style="dashed", color="magenta", weight=3];
7901 -> 7887[label="",style="dashed", color="red", weight=0];
7901[label="compare vz51500 vz515100\n  Integral a",fontsize=16,color="magenta"];7901 -> 7947[label="",style="dashed", color="magenta", weight=3];
7901 -> 7948[label="",style="dashed", color="magenta", weight=3];
7906[label="error []",fontsize=16,color="red",shape="box"];7907[label="error []",fontsize=16,color="red",shape="box"];7908[label="error []",fontsize=16,color="red",shape="box"];7909[label="error []",fontsize=16,color="red",shape="box"];7910[label="error []",fontsize=16,color="red",shape="box"];7911[label="error []",fontsize=16,color="red",shape="box"];7912[label="error []",fontsize=16,color="red",shape="box"];7913[label="error []",fontsize=16,color="red",shape="box"];7914[label="vz51500",fontsize=16,color="green",shape="box"];7915[label="vz5140",fontsize=16,color="green",shape="box"];7917[label="error []",fontsize=16,color="red",shape="box"];7918[label="error []",fontsize=16,color="red",shape="box"];7919[label="error []",fontsize=16,color="red",shape="box"];7920[label="error []",fontsize=16,color="red",shape="box"];8005[label="primMulInt (Pos vz517010) (Pos vz516010)",fontsize=16,color="black",shape="box"];8005 -> 8017[label="",style="solid", color="black", weight=3];
8006[label="primMulInt (Pos vz517010) (Neg vz516010)",fontsize=16,color="black",shape="box"];8006 -> 8018[label="",style="solid", color="black", weight=3];
8007[label="primMulInt (Neg vz517010) (Pos vz516010)",fontsize=16,color="black",shape="box"];8007 -> 8019[label="",style="solid", color="black", weight=3];
8008[label="primMulInt (Neg vz517010) (Neg vz516010)",fontsize=16,color="black",shape="box"];8008 -> 8020[label="",style="solid", color="black", weight=3];
7962[label="primCmpInt (Pos (Succ vz514000)) vz51500",fontsize=16,color="burlywood",shape="box"];8182[label="vz51500/Pos vz515000",fontsize=10,color="white",style="solid",shape="box"];7962 -> 8182[label="",style="solid", color="burlywood", weight=9];
8182 -> 7968[label="",style="solid", color="burlywood", weight=3];
8183[label="vz51500/Neg vz515000",fontsize=10,color="white",style="solid",shape="box"];7962 -> 8183[label="",style="solid", color="burlywood", weight=9];
8183 -> 7969[label="",style="solid", color="burlywood", weight=3];
7963[label="primCmpInt (Pos Zero) vz51500",fontsize=16,color="burlywood",shape="box"];8184[label="vz51500/Pos vz515000",fontsize=10,color="white",style="solid",shape="box"];7963 -> 8184[label="",style="solid", color="burlywood", weight=9];
8184 -> 7970[label="",style="solid", color="burlywood", weight=3];
8185[label="vz51500/Neg vz515000",fontsize=10,color="white",style="solid",shape="box"];7963 -> 8185[label="",style="solid", color="burlywood", weight=9];
8185 -> 7971[label="",style="solid", color="burlywood", weight=3];
7964[label="primCmpInt (Neg (Succ vz514000)) vz51500",fontsize=16,color="burlywood",shape="box"];8186[label="vz51500/Pos vz515000",fontsize=10,color="white",style="solid",shape="box"];7964 -> 8186[label="",style="solid", color="burlywood", weight=9];
8186 -> 7972[label="",style="solid", color="burlywood", weight=3];
8187[label="vz51500/Neg vz515000",fontsize=10,color="white",style="solid",shape="box"];7964 -> 8187[label="",style="solid", color="burlywood", weight=9];
8187 -> 7973[label="",style="solid", color="burlywood", weight=3];
7965[label="primCmpInt (Neg Zero) vz51500",fontsize=16,color="burlywood",shape="box"];8188[label="vz51500/Pos vz515000",fontsize=10,color="white",style="solid",shape="box"];7965 -> 8188[label="",style="solid", color="burlywood", weight=9];
8188 -> 7974[label="",style="solid", color="burlywood", weight=3];
8189[label="vz51500/Neg vz515000",fontsize=10,color="white",style="solid",shape="box"];7965 -> 8189[label="",style="solid", color="burlywood", weight=9];
8189 -> 7975[label="",style="solid", color="burlywood", weight=3];
7921[label="vz515100\n  Ord a",fontsize=16,color="green",shape="box"];7922[label="vz51500\n  Ord a",fontsize=16,color="green",shape="box"];7923[label="vz515100",fontsize=16,color="green",shape="box"];7924[label="vz51500",fontsize=16,color="green",shape="box"];7925[label="vz515100",fontsize=16,color="green",shape="box"];7926[label="vz51500",fontsize=16,color="green",shape="box"];7927[label="vz515100",fontsize=16,color="green",shape="box"];7928[label="vz51500",fontsize=16,color="green",shape="box"];7929[label="vz515100\n  Ord a  Ord b  Ord c",fontsize=16,color="green",shape="box"];7930[label="vz51500\n  Ord a  Ord b  Ord c",fontsize=16,color="green",shape="box"];7931[label="vz515100",fontsize=16,color="green",shape="box"];7932[label="vz51500",fontsize=16,color="green",shape="box"];7933[label="vz515100\n  Ord a",fontsize=16,color="green",shape="box"];7934[label="vz51500\n  Ord a",fontsize=16,color="green",shape="box"];7935[label="vz515100",fontsize=16,color="green",shape="box"];7936[label="vz51500",fontsize=16,color="green",shape="box"];7937[label="vz515100",fontsize=16,color="green",shape="box"];7938[label="vz51500",fontsize=16,color="green",shape="box"];7939[label="vz515100",fontsize=16,color="green",shape="box"];7940[label="vz51500",fontsize=16,color="green",shape="box"];7941[label="vz515100\n  Ord a  Ord b",fontsize=16,color="green",shape="box"];7942[label="vz51500\n  Ord a  Ord b",fontsize=16,color="green",shape="box"];7943[label="vz515100",fontsize=16,color="green",shape="box"];7944[label="vz51500",fontsize=16,color="green",shape="box"];7945[label="vz515100\n  Ord a  Ord b",fontsize=16,color="green",shape="box"];7946[label="vz51500\n  Ord a  Ord b",fontsize=16,color="green",shape="box"];7947[label="vz515100\n  Integral a",fontsize=16,color="green",shape="box"];7948[label="vz51500\n  Integral a",fontsize=16,color="green",shape="box"];8017[label="Pos (primMulNat vz517010 vz516010)",fontsize=16,color="green",shape="box"];8017 -> 8025[label="",style="dashed", color="green", weight=3];
8018[label="Neg (primMulNat vz517010 vz516010)",fontsize=16,color="green",shape="box"];8018 -> 8026[label="",style="dashed", color="green", weight=3];
8019[label="Neg (primMulNat vz517010 vz516010)",fontsize=16,color="green",shape="box"];8019 -> 8027[label="",style="dashed", color="green", weight=3];
8020[label="Pos (primMulNat vz517010 vz516010)",fontsize=16,color="green",shape="box"];8020 -> 8028[label="",style="dashed", color="green", weight=3];
7968[label="primCmpInt (Pos (Succ vz514000)) (Pos vz515000)",fontsize=16,color="black",shape="box"];7968 -> 7979[label="",style="solid", color="black", weight=3];
7969[label="primCmpInt (Pos (Succ vz514000)) (Neg vz515000)",fontsize=16,color="black",shape="box"];7969 -> 7980[label="",style="solid", color="black", weight=3];
7970[label="primCmpInt (Pos Zero) (Pos vz515000)",fontsize=16,color="burlywood",shape="box"];8190[label="vz515000/Succ vz5150000",fontsize=10,color="white",style="solid",shape="box"];7970 -> 8190[label="",style="solid", color="burlywood", weight=9];
8190 -> 7981[label="",style="solid", color="burlywood", weight=3];
8191[label="vz515000/Zero",fontsize=10,color="white",style="solid",shape="box"];7970 -> 8191[label="",style="solid", color="burlywood", weight=9];
8191 -> 7982[label="",style="solid", color="burlywood", weight=3];
7971[label="primCmpInt (Pos Zero) (Neg vz515000)",fontsize=16,color="burlywood",shape="box"];8192[label="vz515000/Succ vz5150000",fontsize=10,color="white",style="solid",shape="box"];7971 -> 8192[label="",style="solid", color="burlywood", weight=9];
8192 -> 7983[label="",style="solid", color="burlywood", weight=3];
8193[label="vz515000/Zero",fontsize=10,color="white",style="solid",shape="box"];7971 -> 8193[label="",style="solid", color="burlywood", weight=9];
8193 -> 7984[label="",style="solid", color="burlywood", weight=3];
7972[label="primCmpInt (Neg (Succ vz514000)) (Pos vz515000)",fontsize=16,color="black",shape="box"];7972 -> 7985[label="",style="solid", color="black", weight=3];
7973[label="primCmpInt (Neg (Succ vz514000)) (Neg vz515000)",fontsize=16,color="black",shape="box"];7973 -> 7986[label="",style="solid", color="black", weight=3];
7974[label="primCmpInt (Neg Zero) (Pos vz515000)",fontsize=16,color="burlywood",shape="box"];8194[label="vz515000/Succ vz5150000",fontsize=10,color="white",style="solid",shape="box"];7974 -> 8194[label="",style="solid", color="burlywood", weight=9];
8194 -> 7987[label="",style="solid", color="burlywood", weight=3];
8195[label="vz515000/Zero",fontsize=10,color="white",style="solid",shape="box"];7974 -> 8195[label="",style="solid", color="burlywood", weight=9];
8195 -> 7988[label="",style="solid", color="burlywood", weight=3];
7975[label="primCmpInt (Neg Zero) (Neg vz515000)",fontsize=16,color="burlywood",shape="box"];8196[label="vz515000/Succ vz5150000",fontsize=10,color="white",style="solid",shape="box"];7975 -> 8196[label="",style="solid", color="burlywood", weight=9];
8196 -> 7989[label="",style="solid", color="burlywood", weight=3];
8197[label="vz515000/Zero",fontsize=10,color="white",style="solid",shape="box"];7975 -> 8197[label="",style="solid", color="burlywood", weight=9];
8197 -> 7990[label="",style="solid", color="burlywood", weight=3];
8025[label="primMulNat vz517010 vz516010",fontsize=16,color="burlywood",shape="triangle"];8198[label="vz517010/Succ vz5170100",fontsize=10,color="white",style="solid",shape="box"];8025 -> 8198[label="",style="solid", color="burlywood", weight=9];
8198 -> 8033[label="",style="solid", color="burlywood", weight=3];
8199[label="vz517010/Zero",fontsize=10,color="white",style="solid",shape="box"];8025 -> 8199[label="",style="solid", color="burlywood", weight=9];
8199 -> 8034[label="",style="solid", color="burlywood", weight=3];
8026 -> 8025[label="",style="dashed", color="red", weight=0];
8026[label="primMulNat vz517010 vz516010",fontsize=16,color="magenta"];8026 -> 8035[label="",style="dashed", color="magenta", weight=3];
8027 -> 8025[label="",style="dashed", color="red", weight=0];
8027[label="primMulNat vz517010 vz516010",fontsize=16,color="magenta"];8027 -> 8036[label="",style="dashed", color="magenta", weight=3];
8028 -> 8025[label="",style="dashed", color="red", weight=0];
8028[label="primMulNat vz517010 vz516010",fontsize=16,color="magenta"];8028 -> 8037[label="",style="dashed", color="magenta", weight=3];
8028 -> 8038[label="",style="dashed", color="magenta", weight=3];
7979[label="primCmpNat (Succ vz514000) vz515000",fontsize=16,color="burlywood",shape="triangle"];8203[label="vz515000/Succ vz5150000",fontsize=10,color="white",style="solid",shape="box"];7979 -> 8203[label="",style="solid", color="burlywood", weight=9];
8203 -> 7993[label="",style="solid", color="burlywood", weight=3];
8204[label="vz515000/Zero",fontsize=10,color="white",style="solid",shape="box"];7979 -> 8204[label="",style="solid", color="burlywood", weight=9];
8204 -> 7994[label="",style="solid", color="burlywood", weight=3];
7980[label="GT",fontsize=16,color="green",shape="box"];7981[label="primCmpInt (Pos Zero) (Pos (Succ vz5150000))",fontsize=16,color="black",shape="box"];7981 -> 7995[label="",style="solid", color="black", weight=3];
7982[label="primCmpInt (Pos Zero) (Pos Zero)",fontsize=16,color="black",shape="box"];7982 -> 7996[label="",style="solid", color="black", weight=3];
7983[label="primCmpInt (Pos Zero) (Neg (Succ vz5150000))",fontsize=16,color="black",shape="box"];7983 -> 7997[label="",style="solid", color="black", weight=3];
7984[label="primCmpInt (Pos Zero) (Neg Zero)",fontsize=16,color="black",shape="box"];7984 -> 7998[label="",style="solid", color="black", weight=3];
7985[label="LT",fontsize=16,color="green",shape="box"];7986[label="primCmpNat vz515000 (Succ vz514000)",fontsize=16,color="burlywood",shape="triangle"];8205[label="vz515000/Succ vz5150000",fontsize=10,color="white",style="solid",shape="box"];7986 -> 8205[label="",style="solid", color="burlywood", weight=9];
8205 -> 7999[label="",style="solid", color="burlywood", weight=3];
8206[label="vz515000/Zero",fontsize=10,color="white",style="solid",shape="box"];7986 -> 8206[label="",style="solid", color="burlywood", weight=9];
8206 -> 8000[label="",style="solid", color="burlywood", weight=3];
7987[label="primCmpInt (Neg Zero) (Pos (Succ vz5150000))",fontsize=16,color="black",shape="box"];7987 -> 8001[label="",style="solid", color="black", weight=3];
7988[label="primCmpInt (Neg Zero) (Pos Zero)",fontsize=16,color="black",shape="box"];7988 -> 8002[label="",style="solid", color="black", weight=3];
7989[label="primCmpInt (Neg Zero) (Neg (Succ vz5150000))",fontsize=16,color="black",shape="box"];7989 -> 8003[label="",style="solid", color="black", weight=3];
7990[label="primCmpInt (Neg Zero) (Neg Zero)",fontsize=16,color="black",shape="box"];7990 -> 8004[label="",style="solid", color="black", weight=3];
8033[label="primMulNat (Succ vz5170100) vz516010",fontsize=16,color="burlywood",shape="box"];8207[label="vz516010/Succ vz5160100",fontsize=10,color="white",style="solid",shape="box"];8033 -> 8207[label="",style="solid", color="burlywood", weight=9];
8207 -> 8043[label="",style="solid", color="burlywood", weight=3];
8208[label="vz516010/Zero",fontsize=10,color="white",style="solid",shape="box"];8033 -> 8208[label="",style="solid", color="burlywood", weight=9];
8208 -> 8044[label="",style="solid", color="burlywood", weight=3];
8034[label="primMulNat Zero vz516010",fontsize=16,color="burlywood",shape="box"];8209[label="vz516010/Succ vz5160100",fontsize=10,color="white",style="solid",shape="box"];8034 -> 8209[label="",style="solid", color="burlywood", weight=9];
8209 -> 8045[label="",style="solid", color="burlywood", weight=3];
8210[label="vz516010/Zero",fontsize=10,color="white",style="solid",shape="box"];8034 -> 8210[label="",style="solid", color="burlywood", weight=9];
8210 -> 8046[label="",style="solid", color="burlywood", weight=3];
8035[label="vz516010",fontsize=16,color="green",shape="box"];8036[label="vz517010",fontsize=16,color="green",shape="box"];8037[label="vz516010",fontsize=16,color="green",shape="box"];8038[label="vz517010",fontsize=16,color="green",shape="box"];7993[label="primCmpNat (Succ vz514000) (Succ vz5150000)",fontsize=16,color="black",shape="box"];7993 -> 8009[label="",style="solid", color="black", weight=3];
7994[label="primCmpNat (Succ vz514000) Zero",fontsize=16,color="black",shape="box"];7994 -> 8010[label="",style="solid", color="black", weight=3];
7995 -> 7986[label="",style="dashed", color="red", weight=0];
7995[label="primCmpNat Zero (Succ vz5150000)",fontsize=16,color="magenta"];7995 -> 8011[label="",style="dashed", color="magenta", weight=3];
7995 -> 8012[label="",style="dashed", color="magenta", weight=3];
7996[label="EQ",fontsize=16,color="green",shape="box"];7997[label="GT",fontsize=16,color="green",shape="box"];7998[label="EQ",fontsize=16,color="green",shape="box"];7999[label="primCmpNat (Succ vz5150000) (Succ vz514000)",fontsize=16,color="black",shape="box"];7999 -> 8013[label="",style="solid", color="black", weight=3];
8000[label="primCmpNat Zero (Succ vz514000)",fontsize=16,color="black",shape="box"];8000 -> 8014[label="",style="solid", color="black", weight=3];
8001[label="LT",fontsize=16,color="green",shape="box"];8002[label="EQ",fontsize=16,color="green",shape="box"];8003 -> 7979[label="",style="dashed", color="red", weight=0];
8003[label="primCmpNat (Succ vz5150000) Zero",fontsize=16,color="magenta"];8003 -> 8015[label="",style="dashed", color="magenta", weight=3];
8003 -> 8016[label="",style="dashed", color="magenta", weight=3];
8004[label="EQ",fontsize=16,color="green",shape="box"];8043[label="primMulNat (Succ vz5170100) (Succ vz5160100)",fontsize=16,color="black",shape="box"];8043 -> 8049[label="",style="solid", color="black", weight=3];
8044[label="primMulNat (Succ vz5170100) Zero",fontsize=16,color="black",shape="box"];8044 -> 8050[label="",style="solid", color="black", weight=3];
8045[label="primMulNat Zero (Succ vz5160100)",fontsize=16,color="black",shape="box"];8045 -> 8051[label="",style="solid", color="black", weight=3];
8046[label="primMulNat Zero Zero",fontsize=16,color="black",shape="box"];8046 -> 8052[label="",style="solid", color="black", weight=3];
8009[label="primCmpNat vz514000 vz5150000",fontsize=16,color="burlywood",shape="triangle"];8213[label="vz514000/Succ vz5140000",fontsize=10,color="white",style="solid",shape="box"];8009 -> 8213[label="",style="solid", color="burlywood", weight=9];
8213 -> 8021[label="",style="solid", color="burlywood", weight=3];
8214[label="vz514000/Zero",fontsize=10,color="white",style="solid",shape="box"];8009 -> 8214[label="",style="solid", color="burlywood", weight=9];
8214 -> 8022[label="",style="solid", color="burlywood", weight=3];
8010[label="GT",fontsize=16,color="green",shape="box"];8011[label="Zero",fontsize=16,color="green",shape="box"];8012[label="vz5150000",fontsize=16,color="green",shape="box"];8013 -> 8009[label="",style="dashed", color="red", weight=0];
8013[label="primCmpNat vz5150000 vz514000",fontsize=16,color="magenta"];8013 -> 8023[label="",style="dashed", color="magenta", weight=3];
8013 -> 8024[label="",style="dashed", color="magenta", weight=3];
8014[label="LT",fontsize=16,color="green",shape="box"];8015[label="Zero",fontsize=16,color="green",shape="box"];8016[label="vz5150000",fontsize=16,color="green",shape="box"];8049 -> 8053[label="",style="dashed", color="red", weight=0];
8049[label="primPlusNat (primMulNat vz5170100 (Succ vz5160100)) (Succ vz5160100)",fontsize=16,color="magenta"];8049 -> 8054[label="",style="dashed", color="magenta", weight=3];
8050[label="Zero",fontsize=16,color="green",shape="box"];8051[label="Zero",fontsize=16,color="green",shape="box"];8052[label="Zero",fontsize=16,color="green",shape="box"];8021[label="primCmpNat (Succ vz5140000) vz5150000",fontsize=16,color="burlywood",shape="box"];8217[label="vz5150000/Succ vz51500000",fontsize=10,color="white",style="solid",shape="box"];8021 -> 8217[label="",style="solid", color="burlywood", weight=9];
8217 -> 8029[label="",style="solid", color="burlywood", weight=3];
8218[label="vz5150000/Zero",fontsize=10,color="white",style="solid",shape="box"];8021 -> 8218[label="",style="solid", color="burlywood", weight=9];
8218 -> 8030[label="",style="solid", color="burlywood", weight=3];
8022[label="primCmpNat Zero vz5150000",fontsize=16,color="burlywood",shape="box"];8219[label="vz5150000/Succ vz51500000",fontsize=10,color="white",style="solid",shape="box"];8022 -> 8219[label="",style="solid", color="burlywood", weight=9];
8219 -> 8031[label="",style="solid", color="burlywood", weight=3];
8220[label="vz5150000/Zero",fontsize=10,color="white",style="solid",shape="box"];8022 -> 8220[label="",style="solid", color="burlywood", weight=9];
8220 -> 8032[label="",style="solid", color="burlywood", weight=3];
8023[label="vz514000",fontsize=16,color="green",shape="box"];8024[label="vz5150000",fontsize=16,color="green",shape="box"];8054 -> 8025[label="",style="dashed", color="red", weight=0];
8054[label="primMulNat vz5170100 (Succ vz5160100)",fontsize=16,color="magenta"];8054 -> 8055[label="",style="dashed", color="magenta", weight=3];
8054 -> 8056[label="",style="dashed", color="magenta", weight=3];
8053[label="primPlusNat vz529 (Succ vz5160100)",fontsize=16,color="burlywood",shape="triangle"];8222[label="vz529/Succ vz5290",fontsize=10,color="white",style="solid",shape="box"];8053 -> 8222[label="",style="solid", color="burlywood", weight=9];
8222 -> 8057[label="",style="solid", color="burlywood", weight=3];
8223[label="vz529/Zero",fontsize=10,color="white",style="solid",shape="box"];8053 -> 8223[label="",style="solid", color="burlywood", weight=9];
8223 -> 8058[label="",style="solid", color="burlywood", weight=3];
8029[label="primCmpNat (Succ vz5140000) (Succ vz51500000)",fontsize=16,color="black",shape="box"];8029 -> 8039[label="",style="solid", color="black", weight=3];
8030[label="primCmpNat (Succ vz5140000) Zero",fontsize=16,color="black",shape="box"];8030 -> 8040[label="",style="solid", color="black", weight=3];
8031[label="primCmpNat Zero (Succ vz51500000)",fontsize=16,color="black",shape="box"];8031 -> 8041[label="",style="solid", color="black", weight=3];
8032[label="primCmpNat Zero Zero",fontsize=16,color="black",shape="box"];8032 -> 8042[label="",style="solid", color="black", weight=3];
8055[label="Succ vz5160100",fontsize=16,color="green",shape="box"];8056[label="vz5170100",fontsize=16,color="green",shape="box"];8057[label="primPlusNat (Succ vz5290) (Succ vz5160100)",fontsize=16,color="black",shape="box"];8057 -> 8059[label="",style="solid", color="black", weight=3];
8058[label="primPlusNat Zero (Succ vz5160100)",fontsize=16,color="black",shape="box"];8058 -> 8060[label="",style="solid", color="black", weight=3];
8039 -> 8009[label="",style="dashed", color="red", weight=0];
8039[label="primCmpNat vz5140000 vz51500000",fontsize=16,color="magenta"];8039 -> 8047[label="",style="dashed", color="magenta", weight=3];
8039 -> 8048[label="",style="dashed", color="magenta", weight=3];
8040[label="GT",fontsize=16,color="green",shape="box"];8041[label="LT",fontsize=16,color="green",shape="box"];8042[label="EQ",fontsize=16,color="green",shape="box"];8059[label="Succ (Succ (primPlusNat vz5290 vz5160100))",fontsize=16,color="green",shape="box"];8059 -> 8061[label="",style="dashed", color="green", weight=3];
8060[label="Succ vz5160100",fontsize=16,color="green",shape="box"];8047[label="vz51500000",fontsize=16,color="green",shape="box"];8048[label="vz5140000",fontsize=16,color="green",shape="box"];8061[label="primPlusNat vz5290 vz5160100",fontsize=16,color="burlywood",shape="triangle"];8225[label="vz5290/Succ vz52900",fontsize=10,color="white",style="solid",shape="box"];8061 -> 8225[label="",style="solid", color="burlywood", weight=9];
8225 -> 8062[label="",style="solid", color="burlywood", weight=3];
8226[label="vz5290/Zero",fontsize=10,color="white",style="solid",shape="box"];8061 -> 8226[label="",style="solid", color="burlywood", weight=9];
8226 -> 8063[label="",style="solid", color="burlywood", weight=3];
8062[label="primPlusNat (Succ vz52900) vz5160100",fontsize=16,color="burlywood",shape="box"];8227[label="vz5160100/Succ vz51601000",fontsize=10,color="white",style="solid",shape="box"];8062 -> 8227[label="",style="solid", color="burlywood", weight=9];
8227 -> 8064[label="",style="solid", color="burlywood", weight=3];
8228[label="vz5160100/Zero",fontsize=10,color="white",style="solid",shape="box"];8062 -> 8228[label="",style="solid", color="burlywood", weight=9];
8228 -> 8065[label="",style="solid", color="burlywood", weight=3];
8063[label="primPlusNat Zero vz5160100",fontsize=16,color="burlywood",shape="box"];8229[label="vz5160100/Succ vz51601000",fontsize=10,color="white",style="solid",shape="box"];8063 -> 8229[label="",style="solid", color="burlywood", weight=9];
8229 -> 8066[label="",style="solid", color="burlywood", weight=3];
8230[label="vz5160100/Zero",fontsize=10,color="white",style="solid",shape="box"];8063 -> 8230[label="",style="solid", color="burlywood", weight=9];
8230 -> 8067[label="",style="solid", color="burlywood", weight=3];
8064[label="primPlusNat (Succ vz52900) (Succ vz51601000)",fontsize=16,color="black",shape="box"];8064 -> 8068[label="",style="solid", color="black", weight=3];
8065[label="primPlusNat (Succ vz52900) Zero",fontsize=16,color="black",shape="box"];8065 -> 8069[label="",style="solid", color="black", weight=3];
8066[label="primPlusNat Zero (Succ vz51601000)",fontsize=16,color="black",shape="box"];8066 -> 8070[label="",style="solid", color="black", weight=3];
8067[label="primPlusNat Zero Zero",fontsize=16,color="black",shape="box"];8067 -> 8071[label="",style="solid", color="black", weight=3];
8068[label="Succ (Succ (primPlusNat vz52900 vz51601000))",fontsize=16,color="green",shape="box"];8068 -> 8072[label="",style="dashed", color="green", weight=3];
8069[label="Succ vz52900",fontsize=16,color="green",shape="box"];8070[label="Succ vz51601000",fontsize=16,color="green",shape="box"];8071[label="Zero",fontsize=16,color="green",shape="box"];8072 -> 8061[label="",style="dashed", color="red", weight=0];
8072[label="primPlusNat vz52900 vz51601000",fontsize=16,color="magenta"];8072 -> 8073[label="",style="dashed", color="magenta", weight=3];
8072 -> 8074[label="",style="dashed", color="magenta", weight=3];
8073[label="vz52900",fontsize=16,color="green",shape="box"];8074[label="vz51601000",fontsize=16,color="green",shape="box"];}

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                    ↳ QDPSizeChangeProof

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_map(:(vz3110, vz3111)) → new_map(vz3111)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

new_map(:(vz3110, vz3111)) → new_map(vz3111)
The graph contains the following edges 1 > 1

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPSizeChangeProof

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(vz52900), Succ(vz51601000)) → new_primPlusNat(vz52900, vz51601000)

From the DPs we obtained the following set of size-change graphs:

new_primPlusNat(Succ(vz52900), Succ(vz51601000)) → new_primPlusNat(vz52900, vz51601000)
The graph contains the following edges 1 > 1, 2 > 2

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPSizeChangeProof

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(vz5170100), Succ(vz5160100)) → new_primMulNat(vz5170100, Succ(vz5160100))

From the DPs we obtained the following set of size-change graphs:

new_primMulNat(Succ(vz5170100), Succ(vz5160100)) → new_primMulNat(vz5170100, Succ(vz5160100))
The graph contains the following edges 1 > 1, 2 >= 2

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPSizeChangeProof

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primCmpNat(Succ(vz5140000), Succ(vz51500000)) → new_primCmpNat(vz5140000, vz51500000)

From the DPs we obtained the following set of size-change graphs:

new_primCmpNat(Succ(vz5140000), Succ(vz51500000)) → new_primCmpNat(vz5140000, vz51500000)
The graph contains the following edges 1 > 1, 2 > 2

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPOrderProof

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_merge0(vz524, vz525, vz526, vz527, GT, ba) → new_merge(:(vz525, vz526), vz527, ba)
new_merge0(vz524, vz525, vz526, vz527, EQ, ba) → new_merge(vz526, :(vz524, vz527), ba)
new_merge(:(vz5140, vz5141), :(vz51500, vz51501), bb) → new_merge0(vz51500, vz5140, vz5141, vz51501, new_compare(vz5140, vz51500, bb), bb)
new_merge0(vz524, vz525, vz526, vz527, LT, ba) → new_merge(vz526, :(vz524, vz527), ba)

The TRS R consists of the following rules:

new_sr(Neg(vz517010), Neg(vz516010)) → Pos(new_primMulNat0(vz517010, vz516010))
new_compare7(vz5140, vz51500, bg, bh) → error([])
new_primCmpNat1(Succ(vz5140000), Succ(vz51500000)) → new_primCmpNat1(vz5140000, vz51500000)
new_primCmpNat0(Succ(vz5150000), vz514000) → new_primCmpNat1(vz5150000, vz514000)
new_compare10(vz5140, vz51500) → error([])
new_sr(Pos(vz517010), Pos(vz516010)) → Pos(new_primMulNat0(vz517010, vz516010))
new_primPlusNat1(Succ(vz52900), Succ(vz51601000)) → Succ(Succ(new_primPlusNat1(vz52900, vz51601000)))
new_compare(vz5140, vz51500, app(ty_Maybe, bc)) → new_compare0(vz5140, vz51500, bc)
new_compare(vz5140, vz51500, ty_Int) → new_compare13(vz5140, vz51500)
new_primMulNat0(Succ(vz5170100), Zero) → Zero
new_primMulNat0(Zero, Succ(vz5160100)) → Zero
new_compare13(Neg(Succ(vz514000)), Pos(vz515000)) → LT
new_compare(vz5140, vz51500, app(app(ty_@2, bd), be)) → new_compare2(vz5140, vz51500, bd, be)
new_compare2(vz5140, vz51500, bd, be) → error([])
new_compare(vz5140, vz51500, app(ty_Ratio, ca)) → new_compare8(vz5140, vz51500, ca)
new_compare12(Float(vz51700, vz51701), Float(vz51600, vz51601)) → new_compare13(new_sr(vz51700, vz51600), new_sr(vz51701, vz51601))
new_compare(vz5140, vz51500, app(app(ty_Either, bg), bh)) → new_compare7(vz5140, vz51500, bg, bh)
new_compare(vz5140, vz51500, ty_Bool) → new_compare3(vz5140, vz51500)
new_primCmpNat2(vz514000, Zero) → GT
new_compare0(vz5140, vz51500, bc) → error([])
new_primPlusNat1(Zero, Zero) → Zero
new_compare(vz5140, vz51500, ty_Char) → new_compare9(vz5140, vz51500)
new_primCmpNat1(Zero, Succ(vz51500000)) → LT
new_compare13(Neg(Zero), Neg(Succ(vz5150000))) → new_primCmpNat2(vz5150000, Zero)
new_primMulNat0(Succ(vz5170100), Succ(vz5160100)) → new_primPlusNat0(new_primMulNat0(vz5170100, Succ(vz5160100)), vz5160100)
new_compare9(vz5140, vz51500) → error([])
new_primCmpNat0(Zero, vz514000) → LT
new_compare3(vz5140, vz51500) → error([])
new_compare(vz5140, vz51500, ty_Integer) → new_compare10(vz5140, vz51500)
new_primCmpNat1(Zero, Zero) → EQ
new_compare4(vz5140, vz51500, bf) → error([])
new_compare(vz5140, vz51500, ty_Float) → new_compare12(vz5140, vz51500)
new_primMulNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(vz5290), vz5160100) → Succ(Succ(new_primPlusNat1(vz5290, vz5160100)))
new_compare(vz5140, vz51500, ty_Double) → new_compare6(vz5140, vz51500)
new_compare(vz5140, vz51500, app(ty_[], bf)) → new_compare4(vz5140, vz51500, bf)
new_compare13(Pos(Zero), Pos(Succ(vz5150000))) → new_primCmpNat0(Zero, vz5150000)
new_primPlusNat0(Zero, vz5160100) → Succ(vz5160100)
new_compare11(vz5140, vz51500, cb, cc, cd) → error([])
new_compare13(Neg(Zero), Neg(Zero)) → EQ
new_primCmpNat1(Succ(vz5140000), Zero) → GT
new_compare1(vz5140, vz51500) → error([])
new_compare(vz5140, vz51500, ty_@0) → new_compare1(vz5140, vz51500)
new_compare6(vz5140, vz51500) → error([])
new_compare13(Pos(Zero), Neg(Succ(vz5150000))) → GT
new_compare8(vz5140, vz51500, ca) → error([])
new_compare5(vz5140, vz51500) → error([])
new_compare13(Pos(Succ(vz514000)), Pos(vz515000)) → new_primCmpNat2(vz514000, vz515000)
new_compare(vz5140, vz51500, ty_Ordering) → new_compare5(vz5140, vz51500)
new_compare13(Neg(Zero), Pos(Zero)) → EQ
new_compare13(Pos(Zero), Neg(Zero)) → EQ
new_primPlusNat1(Succ(vz52900), Zero) → Succ(vz52900)
new_primPlusNat1(Zero, Succ(vz51601000)) → Succ(vz51601000)
new_compare13(Neg(Zero), Pos(Succ(vz5150000))) → LT
new_sr(Neg(vz517010), Pos(vz516010)) → Neg(new_primMulNat0(vz517010, vz516010))
new_sr(Pos(vz517010), Neg(vz516010)) → Neg(new_primMulNat0(vz517010, vz516010))
new_compare(vz5140, vz51500, app(app(app(ty_@3, cb), cc), cd)) → new_compare11(vz5140, vz51500, cb, cc, cd)
new_compare13(Pos(Zero), Pos(Zero)) → EQ
new_primCmpNat2(vz514000, Succ(vz5150000)) → new_primCmpNat1(vz514000, vz5150000)
new_compare13(Neg(Succ(vz514000)), Neg(vz515000)) → new_primCmpNat0(vz515000, vz514000)
new_compare13(Pos(Succ(vz514000)), Neg(vz515000)) → GT

The set Q consists of the following terms:

new_compare13(Pos(Succ(x0)), Neg(x1))
new_compare13(Neg(Succ(x0)), Pos(x1))
new_primCmpNat1(Succ(x0), Zero)
new_compare8(x0, x1, x2)
new_primCmpNat2(x0, Zero)
new_primCmpNat2(x0, Succ(x1))
new_primMulNat0(Zero, Zero)
new_compare(x0, x1, ty_Integer)
new_compare(x0, x1, ty_@0)
new_primCmpNat0(Zero, x0)
new_compare(x0, x1, app(ty_[], x2))
new_compare11(x0, x1, x2, x3, x4)
new_sr(Neg(x0), Pos(x1))
new_sr(Pos(x0), Neg(x1))
new_compare2(x0, x1, x2, x3)
new_primCmpNat1(Succ(x0), Succ(x1))
new_primPlusNat1(Zero, Zero)
new_compare(x0, x1, ty_Ordering)
new_primMulNat0(Succ(x0), Zero)
new_compare5(x0, x1)
new_primPlusNat1(Succ(x0), Zero)
new_compare(x0, x1, ty_Char)
new_primCmpNat1(Zero, Zero)
new_sr(Pos(x0), Pos(x1))
new_primPlusNat1(Zero, Succ(x0))
new_primCmpNat1(Zero, Succ(x0))
new_compare1(x0, x1)
new_compare13(Pos(Zero), Pos(Succ(x0)))
new_compare13(Neg(Succ(x0)), Neg(x1))
new_compare(x0, x1, app(app(ty_Either, x2), x3))
new_compare4(x0, x1, x2)
new_compare13(Neg(Zero), Pos(Zero))
new_compare13(Pos(Zero), Neg(Zero))
new_primCmpNat0(Succ(x0), x1)
new_primPlusNat0(Zero, x0)
new_compare12(Float(x0, x1), Float(x2, x3))
new_compare10(x0, x1)
new_compare0(x0, x1, x2)
new_compare(x0, x1, app(app(ty_@2, x2), x3))
new_compare6(x0, x1)
new_compare13(Neg(Zero), Neg(Succ(x0)))
new_compare(x0, x1, app(ty_Ratio, x2))
new_compare(x0, x1, app(ty_Maybe, x2))
new_primPlusNat0(Succ(x0), x1)
new_compare9(x0, x1)
new_sr(Neg(x0), Neg(x1))
new_compare(x0, x1, ty_Int)
new_compare3(x0, x1)
new_compare7(x0, x1, x2, x3)
new_primMulNat0(Succ(x0), Succ(x1))
new_compare13(Neg(Zero), Pos(Succ(x0)))
new_compare(x0, x1, ty_Double)
new_compare13(Pos(Zero), Neg(Succ(x0)))
new_compare13(Pos(Succ(x0)), Pos(x1))
new_compare13(Neg(Zero), Neg(Zero))
new_primMulNat0(Zero, Succ(x0))
new_compare(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_compare(x0, x1, ty_Float)
new_compare(x0, x1, ty_Bool)
new_primPlusNat1(Succ(x0), Succ(x1))
new_compare13(Pos(Zero), Pos(Zero))

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

new_merge0(vz524, vz525, vz526, vz527, EQ, ba) → new_merge(vz526, :(vz524, vz527), ba)
new_merge0(vz524, vz525, vz526, vz527, LT, ba) → new_merge(vz526, :(vz524, vz527), ba)

The remaining pairs can at least be oriented weakly.

new_merge0(vz524, vz525, vz526, vz527, GT, ba) → new_merge(:(vz525, vz526), vz527, ba)
new_merge(:(vz5140, vz5141), :(vz51500, vz51501), bb) → new_merge0(vz51500, vz5140, vz5141, vz51501, new_compare(vz5140, vz51500, bb), bb)

Used ordering: Polynomial interpretation [25]:

POL(:(x₁, x₂)) = 1 + x₁ + x₂
POL(EQ) = 0
POL(Float(x₁, x₂)) = 0
POL(GT) = 0
POL(LT) = 0
POL(Neg(x₁)) = 0
POL(Pos(x₁)) = 0
POL(Succ(x₁)) = 1
POL(Zero) = 1
POL([]) = 0
POL(app(x₁, x₂)) = 0
POL(error(x₁)) = 0
POL(new_compare(x₁, x₂, x₃)) = 0
POL(new_compare0(x₁, x₂, x₃)) = 0
POL(new_compare1(x₁, x₂)) = 0
POL(new_compare10(x₁, x₂)) = 0
POL(new_compare11(x₁, x₂, x₃, x₄, x₅)) = 0
POL(new_compare12(x₁, x₂)) = 0
POL(new_compare13(x₁, x₂)) = 0
POL(new_compare2(x₁, x₂, x₃, x₄)) = 0
POL(new_compare3(x₁, x₂)) = 0
POL(new_compare4(x₁, x₂, x₃)) = 0
POL(new_compare5(x₁, x₂)) = 0
POL(new_compare6(x₁, x₂)) = 0
POL(new_compare7(x₁, x₂, x₃, x₄)) = 0
POL(new_compare8(x₁, x₂, x₃)) = 0
POL(new_compare9(x₁, x₂)) = 0
POL(new_merge(x₁, x₂, x₃)) = x₁
POL(new_merge0(x₁, x₂, x₃, x₄, x₅, x₆)) = 1 + x₂ + x₃
POL(new_primCmpNat0(x₁, x₂)) = 0
POL(new_primCmpNat1(x₁, x₂)) = 0
POL(new_primCmpNat2(x₁, x₂)) = 0
POL(new_primMulNat0(x₁, x₂)) = 0
POL(new_primPlusNat0(x₁, x₂)) = 0
POL(new_primPlusNat1(x₁, x₂)) = 1 + x₁
POL(new_sr(x₁, x₂)) = 0
POL(ty_@0) = 0
POL(ty_@2) = 0
POL(ty_@3) = 0
POL(ty_Bool) = 0
POL(ty_Char) = 0
POL(ty_Double) = 0
POL(ty_Either) = 0
POL(ty_Float) = 0
POL(ty_Int) = 0
POL(ty_Integer) = 0
POL(ty_Maybe) = 0
POL(ty_Ordering) = 0
POL(ty_Ratio) = 0
POL(ty_[]) = 0

The following usable rules [17] were oriented: none

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPOrderProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_merge0(vz524, vz525, vz526, vz527, GT, ba) → new_merge(:(vz525, vz526), vz527, ba)
new_merge(:(vz5140, vz5141), :(vz51500, vz51501), bb) → new_merge0(vz51500, vz5140, vz5141, vz51501, new_compare(vz5140, vz51500, bb), bb)

The TRS R consists of the following rules:

new_sr(Neg(vz517010), Neg(vz516010)) → Pos(new_primMulNat0(vz517010, vz516010))
new_compare7(vz5140, vz51500, bg, bh) → error([])
new_primCmpNat1(Succ(vz5140000), Succ(vz51500000)) → new_primCmpNat1(vz5140000, vz51500000)
new_primCmpNat0(Succ(vz5150000), vz514000) → new_primCmpNat1(vz5150000, vz514000)
new_compare10(vz5140, vz51500) → error([])
new_sr(Pos(vz517010), Pos(vz516010)) → Pos(new_primMulNat0(vz517010, vz516010))
new_primPlusNat1(Succ(vz52900), Succ(vz51601000)) → Succ(Succ(new_primPlusNat1(vz52900, vz51601000)))
new_compare(vz5140, vz51500, app(ty_Maybe, bc)) → new_compare0(vz5140, vz51500, bc)
new_compare(vz5140, vz51500, ty_Int) → new_compare13(vz5140, vz51500)
new_primMulNat0(Succ(vz5170100), Zero) → Zero
new_primMulNat0(Zero, Succ(vz5160100)) → Zero
new_compare13(Neg(Succ(vz514000)), Pos(vz515000)) → LT
new_compare(vz5140, vz51500, app(app(ty_@2, bd), be)) → new_compare2(vz5140, vz51500, bd, be)
new_compare2(vz5140, vz51500, bd, be) → error([])
new_compare(vz5140, vz51500, app(ty_Ratio, ca)) → new_compare8(vz5140, vz51500, ca)
new_compare12(Float(vz51700, vz51701), Float(vz51600, vz51601)) → new_compare13(new_sr(vz51700, vz51600), new_sr(vz51701, vz51601))
new_compare(vz5140, vz51500, app(app(ty_Either, bg), bh)) → new_compare7(vz5140, vz51500, bg, bh)
new_compare(vz5140, vz51500, ty_Bool) → new_compare3(vz5140, vz51500)
new_primCmpNat2(vz514000, Zero) → GT
new_compare0(vz5140, vz51500, bc) → error([])
new_primPlusNat1(Zero, Zero) → Zero
new_compare(vz5140, vz51500, ty_Char) → new_compare9(vz5140, vz51500)
new_primCmpNat1(Zero, Succ(vz51500000)) → LT
new_compare13(Neg(Zero), Neg(Succ(vz5150000))) → new_primCmpNat2(vz5150000, Zero)
new_primMulNat0(Succ(vz5170100), Succ(vz5160100)) → new_primPlusNat0(new_primMulNat0(vz5170100, Succ(vz5160100)), vz5160100)
new_compare9(vz5140, vz51500) → error([])
new_primCmpNat0(Zero, vz514000) → LT
new_compare3(vz5140, vz51500) → error([])
new_compare(vz5140, vz51500, ty_Integer) → new_compare10(vz5140, vz51500)
new_primCmpNat1(Zero, Zero) → EQ
new_compare4(vz5140, vz51500, bf) → error([])
new_compare(vz5140, vz51500, ty_Float) → new_compare12(vz5140, vz51500)
new_primMulNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(vz5290), vz5160100) → Succ(Succ(new_primPlusNat1(vz5290, vz5160100)))
new_compare(vz5140, vz51500, ty_Double) → new_compare6(vz5140, vz51500)
new_compare(vz5140, vz51500, app(ty_[], bf)) → new_compare4(vz5140, vz51500, bf)
new_compare13(Pos(Zero), Pos(Succ(vz5150000))) → new_primCmpNat0(Zero, vz5150000)
new_primPlusNat0(Zero, vz5160100) → Succ(vz5160100)
new_compare11(vz5140, vz51500, cb, cc, cd) → error([])
new_compare13(Neg(Zero), Neg(Zero)) → EQ
new_primCmpNat1(Succ(vz5140000), Zero) → GT
new_compare1(vz5140, vz51500) → error([])
new_compare(vz5140, vz51500, ty_@0) → new_compare1(vz5140, vz51500)
new_compare6(vz5140, vz51500) → error([])
new_compare13(Pos(Zero), Neg(Succ(vz5150000))) → GT
new_compare8(vz5140, vz51500, ca) → error([])
new_compare5(vz5140, vz51500) → error([])
new_compare13(Pos(Succ(vz514000)), Pos(vz515000)) → new_primCmpNat2(vz514000, vz515000)
new_compare(vz5140, vz51500, ty_Ordering) → new_compare5(vz5140, vz51500)
new_compare13(Neg(Zero), Pos(Zero)) → EQ
new_compare13(Pos(Zero), Neg(Zero)) → EQ
new_primPlusNat1(Succ(vz52900), Zero) → Succ(vz52900)
new_primPlusNat1(Zero, Succ(vz51601000)) → Succ(vz51601000)
new_compare13(Neg(Zero), Pos(Succ(vz5150000))) → LT
new_sr(Neg(vz517010), Pos(vz516010)) → Neg(new_primMulNat0(vz517010, vz516010))
new_sr(Pos(vz517010), Neg(vz516010)) → Neg(new_primMulNat0(vz517010, vz516010))
new_compare(vz5140, vz51500, app(app(app(ty_@3, cb), cc), cd)) → new_compare11(vz5140, vz51500, cb, cc, cd)
new_compare13(Pos(Zero), Pos(Zero)) → EQ
new_primCmpNat2(vz514000, Succ(vz5150000)) → new_primCmpNat1(vz514000, vz5150000)
new_compare13(Neg(Succ(vz514000)), Neg(vz515000)) → new_primCmpNat0(vz515000, vz514000)
new_compare13(Pos(Succ(vz514000)), Neg(vz515000)) → GT

The set Q consists of the following terms:

new_compare13(Pos(Succ(x0)), Neg(x1))
new_compare13(Neg(Succ(x0)), Pos(x1))
new_primCmpNat1(Succ(x0), Zero)
new_compare8(x0, x1, x2)
new_primCmpNat2(x0, Zero)
new_primCmpNat2(x0, Succ(x1))
new_primMulNat0(Zero, Zero)
new_compare(x0, x1, ty_Integer)
new_compare(x0, x1, ty_@0)
new_primCmpNat0(Zero, x0)
new_compare(x0, x1, app(ty_[], x2))
new_compare11(x0, x1, x2, x3, x4)
new_sr(Neg(x0), Pos(x1))
new_sr(Pos(x0), Neg(x1))
new_compare2(x0, x1, x2, x3)
new_primCmpNat1(Succ(x0), Succ(x1))
new_primPlusNat1(Zero, Zero)
new_compare(x0, x1, ty_Ordering)
new_primMulNat0(Succ(x0), Zero)
new_compare5(x0, x1)
new_primPlusNat1(Succ(x0), Zero)
new_compare(x0, x1, ty_Char)
new_primCmpNat1(Zero, Zero)
new_sr(Pos(x0), Pos(x1))
new_primPlusNat1(Zero, Succ(x0))
new_primCmpNat1(Zero, Succ(x0))
new_compare1(x0, x1)
new_compare13(Pos(Zero), Pos(Succ(x0)))
new_compare13(Neg(Succ(x0)), Neg(x1))
new_compare(x0, x1, app(app(ty_Either, x2), x3))
new_compare4(x0, x1, x2)
new_compare13(Neg(Zero), Pos(Zero))
new_compare13(Pos(Zero), Neg(Zero))
new_primCmpNat0(Succ(x0), x1)
new_primPlusNat0(Zero, x0)
new_compare12(Float(x0, x1), Float(x2, x3))
new_compare10(x0, x1)
new_compare0(x0, x1, x2)
new_compare(x0, x1, app(app(ty_@2, x2), x3))
new_compare6(x0, x1)
new_compare13(Neg(Zero), Neg(Succ(x0)))
new_compare(x0, x1, app(ty_Ratio, x2))
new_compare(x0, x1, app(ty_Maybe, x2))
new_primPlusNat0(Succ(x0), x1)
new_compare9(x0, x1)
new_sr(Neg(x0), Neg(x1))
new_compare(x0, x1, ty_Int)
new_compare3(x0, x1)
new_compare7(x0, x1, x2, x3)
new_primMulNat0(Succ(x0), Succ(x1))
new_compare13(Neg(Zero), Pos(Succ(x0)))
new_compare(x0, x1, ty_Double)
new_compare13(Pos(Zero), Neg(Succ(x0)))
new_compare13(Pos(Succ(x0)), Pos(x1))
new_compare13(Neg(Zero), Neg(Zero))
new_primMulNat0(Zero, Succ(x0))
new_compare(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_compare(x0, x1, ty_Float)
new_compare(x0, x1, ty_Bool)
new_primPlusNat1(Succ(x0), Succ(x1))
new_compare13(Pos(Zero), Pos(Zero))

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

new_merge(:(vz5140, vz5141), :(vz51500, vz51501), bb) → new_merge0(vz51500, vz5140, vz5141, vz51501, new_compare(vz5140, vz51500, bb), bb)
The graph contains the following edges 2 > 1, 1 > 2, 1 > 3, 2 > 4, 3 >= 6
new_merge0(vz524, vz525, vz526, vz527, GT, ba) → new_merge(:(vz525, vz526), vz527, ba)
The graph contains the following edges 4 >= 2, 6 >= 3

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPSizeChangeProof

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_merge_pairs(:(vz515110, :(vz5151110, vz5151111)), ba) → new_merge_pairs(vz5151111, ba)

From the DPs we obtained the following set of size-change graphs:

new_merge_pairs(:(vz515110, :(vz5151110, vz5151111)), ba) → new_merge_pairs(vz5151111, ba)
The graph contains the following edges 1 > 1, 2 >= 2

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

new_mergesort'(vz514, :(vz5150, []), ba) → new_mergesort'(new_merge2(vz514, vz5150, ba), [], ba)
new_mergesort'(vz514, :(vz5150, :(vz51510, vz51511)), ba) → new_mergesort'(new_merge1(vz514, vz5150, vz51510, ba), new_merge_pairs0(vz51511, ba), ba)

The TRS R consists of the following rules:

new_sr(Neg(vz517010), Neg(vz516010)) → Pos(new_primMulNat0(vz517010, vz516010))
new_compare7(vz5140, vz51500, bc, bd) → error([])
new_primCmpNat1(Succ(vz5140000), Succ(vz51500000)) → new_primCmpNat1(vz5140000, vz51500000)
new_primCmpNat0(Succ(vz5150000), vz514000) → new_primCmpNat1(vz5150000, vz514000)
new_compare10(vz5140, vz51500) → error([])
new_sr(Pos(vz517010), Pos(vz516010)) → Pos(new_primMulNat0(vz517010, vz516010))
new_merge00(vz524, vz525, vz526, vz527, LT, be) → :(vz525, new_merge2(vz526, :(vz524, vz527), be))
new_compare14(vz51500, vz515100, app(ty_Ratio, ca)) → new_compare8(vz51500, vz515100, ca)
new_compare(vz5140, vz51500, app(ty_Maybe, bb)) → new_compare0(vz5140, vz51500, bb)
new_primPlusNat1(Succ(vz52900), Succ(vz51601000)) → Succ(Succ(new_primPlusNat1(vz52900, vz51601000)))
new_merge_pairs0(:(vz515110, :(vz5151110, vz5151111)), ba) → :(new_merge2(vz515110, vz5151110, ba), new_merge_pairs0(vz5151111, ba))
new_compare14(vz51500, vz515100, app(app(app(ty_@3, cb), cc), cd)) → new_compare11(vz51500, vz515100, cb, cc, cd)
new_compare(vz5140, vz51500, ty_Int) → new_compare13(vz5140, vz51500)
new_merge1(vz514, [], :(vz515100, vz515101), ba) → new_merge2(vz514, :(vz515100, vz515101), ba)
new_merge_pairs0(:(vz515110, []), ba) → :(vz515110, [])
new_primMulNat0(Succ(vz5170100), Zero) → Zero
new_primMulNat0(Zero, Succ(vz5160100)) → Zero
new_compare13(Neg(Succ(vz514000)), Pos(vz515000)) → LT
new_compare(vz5140, vz51500, app(app(ty_@2, bf), bg)) → new_compare2(vz5140, vz51500, bf, bg)
new_compare2(vz5140, vz51500, bf, bg) → error([])
new_compare(vz5140, vz51500, app(ty_Ratio, ca)) → new_compare8(vz5140, vz51500, ca)
new_compare12(Float(vz51700, vz51701), Float(vz51600, vz51601)) → new_compare13(new_sr(vz51700, vz51600), new_sr(vz51701, vz51601))
new_compare(vz5140, vz51500, app(app(ty_Either, bc), bd)) → new_compare7(vz5140, vz51500, bc, bd)
new_compare(vz5140, vz51500, ty_Bool) → new_compare3(vz5140, vz51500)
new_primCmpNat2(vz514000, Zero) → GT
new_merge1(vz514, :(vz51500, vz51501), :(vz515100, vz515101), ba) → new_merge2(vz514, new_merge00(vz515100, vz51500, vz51501, vz515101, new_compare14(vz51500, vz515100, ba), ba), ba)
new_compare0(vz5140, vz51500, bb) → error([])
new_primPlusNat1(Zero, Zero) → Zero
new_compare(vz5140, vz51500, ty_Char) → new_compare9(vz5140, vz51500)
new_primCmpNat1(Zero, Succ(vz51500000)) → LT
new_compare13(Neg(Zero), Neg(Succ(vz5150000))) → new_primCmpNat2(vz5150000, Zero)
new_compare14(vz51500, vz515100, ty_Bool) → new_compare3(vz51500, vz515100)
new_merge00(vz524, vz525, vz526, vz527, GT, be) → :(vz524, new_merge2(:(vz525, vz526), vz527, be))
new_primMulNat0(Succ(vz5170100), Succ(vz5160100)) → new_primPlusNat0(new_primMulNat0(vz5170100, Succ(vz5160100)), vz5160100)
new_compare14(vz51500, vz515100, ty_Integer) → new_compare10(vz51500, vz515100)
new_compare9(vz5140, vz51500) → error([])
new_compare14(vz51500, vz515100, ty_Char) → new_compare9(vz51500, vz515100)
new_primCmpNat0(Zero, vz514000) → LT
new_compare3(vz5140, vz51500) → error([])
new_compare(vz5140, vz51500, ty_Integer) → new_compare10(vz5140, vz51500)
new_primCmpNat1(Zero, Zero) → EQ
new_compare4(vz5140, vz51500, bh) → error([])
new_merge2([], :(vz51500, vz51501), ba) → :(vz51500, vz51501)
new_compare(vz5140, vz51500, ty_Float) → new_compare12(vz5140, vz51500)
new_primMulNat0(Zero, Zero) → Zero
new_merge_pairs0([], ba) → []
new_compare14(vz51500, vz515100, app(ty_Maybe, bb)) → new_compare0(vz51500, vz515100, bb)
new_compare14(vz51500, vz515100, ty_Double) → new_compare6(vz51500, vz515100)
new_compare14(vz51500, vz515100, ty_Int) → new_compare13(vz51500, vz515100)
new_primPlusNat0(Succ(vz5290), vz5160100) → Succ(Succ(new_primPlusNat1(vz5290, vz5160100)))
new_compare14(vz51500, vz515100, app(ty_[], bh)) → new_compare4(vz51500, vz515100, bh)
new_compare(vz5140, vz51500, ty_Double) → new_compare6(vz5140, vz51500)
new_merge1(vz514, vz5150, [], ba) → new_merge2(vz514, vz5150, ba)
new_merge2(:(vz5140, vz5141), :(vz51500, vz51501), ba) → new_merge00(vz51500, vz5140, vz5141, vz51501, new_compare(vz5140, vz51500, ba), ba)
new_compare(vz5140, vz51500, app(ty_[], bh)) → new_compare4(vz5140, vz51500, bh)
new_compare14(vz51500, vz515100, ty_Float) → new_compare12(vz51500, vz515100)
new_compare14(vz51500, vz515100, ty_@0) → new_compare1(vz51500, vz515100)
new_compare14(vz51500, vz515100, app(app(ty_@2, bf), bg)) → new_compare2(vz51500, vz515100, bf, bg)
new_compare13(Pos(Zero), Pos(Succ(vz5150000))) → new_primCmpNat0(Zero, vz5150000)
new_primPlusNat0(Zero, vz5160100) → Succ(vz5160100)
new_compare11(vz5140, vz51500, cb, cc, cd) → error([])
new_merge2(vz514, [], ba) → vz514
new_compare13(Neg(Zero), Neg(Zero)) → EQ
new_primCmpNat1(Succ(vz5140000), Zero) → GT
new_compare14(vz51500, vz515100, app(app(ty_Either, bc), bd)) → new_compare7(vz51500, vz515100, bc, bd)
new_compare1(vz5140, vz51500) → error([])
new_compare(vz5140, vz51500, ty_@0) → new_compare1(vz5140, vz51500)
new_compare6(vz5140, vz51500) → error([])
new_compare13(Pos(Zero), Neg(Succ(vz5150000))) → GT
new_compare8(vz5140, vz51500, ca) → error([])
new_compare5(vz5140, vz51500) → error([])
new_compare13(Pos(Succ(vz514000)), Pos(vz515000)) → new_primCmpNat2(vz514000, vz515000)
new_compare(vz5140, vz51500, ty_Ordering) → new_compare5(vz5140, vz51500)
new_compare13(Pos(Zero), Neg(Zero)) → EQ
new_compare13(Neg(Zero), Pos(Zero)) → EQ
new_primPlusNat1(Succ(vz52900), Zero) → Succ(vz52900)
new_primPlusNat1(Zero, Succ(vz51601000)) → Succ(vz51601000)
new_compare13(Neg(Zero), Pos(Succ(vz5150000))) → LT
new_sr(Neg(vz517010), Pos(vz516010)) → Neg(new_primMulNat0(vz517010, vz516010))
new_sr(Pos(vz517010), Neg(vz516010)) → Neg(new_primMulNat0(vz517010, vz516010))
new_compare(vz5140, vz51500, app(app(app(ty_@3, cb), cc), cd)) → new_compare11(vz5140, vz51500, cb, cc, cd)
new_merge00(vz524, vz525, vz526, vz527, EQ, be) → :(vz525, new_merge2(vz526, :(vz524, vz527), be))
new_compare14(vz51500, vz515100, ty_Ordering) → new_compare5(vz51500, vz515100)
new_compare13(Pos(Zero), Pos(Zero)) → EQ
new_primCmpNat2(vz514000, Succ(vz5150000)) → new_primCmpNat1(vz514000, vz5150000)
new_compare13(Neg(Succ(vz514000)), Neg(vz515000)) → new_primCmpNat0(vz515000, vz514000)
new_compare13(Pos(Succ(vz514000)), Neg(vz515000)) → GT

The set Q consists of the following terms:

new_compare13(Pos(Succ(x0)), Neg(x1))
new_primCmpNat1(Succ(x0), Zero)
new_compare13(Neg(Succ(x0)), Pos(x1))
new_compare8(x0, x1, x2)
new_compare14(x0, x1, app(ty_Ratio, x2))
new_compare14(x0, x1, app(app(ty_Either, x2), x3))
new_compare2(x0, x1, x2, x3)
new_primCmpNat2(x0, Zero)
new_primCmpNat2(x0, Succ(x1))
new_compare14(x0, x1, app(ty_[], x2))
new_compare(x0, x1, app(app(ty_@2, x2), x3))
new_merge1(x0, [], :(x1, x2), x3)
new_primMulNat0(Zero, Zero)
new_compare(x0, x1, ty_@0)
new_compare(x0, x1, ty_Integer)
new_primCmpNat0(Zero, x0)
new_merge00(x0, x1, x2, x3, GT, x4)
new_compare11(x0, x1, x2, x3, x4)
new_sr(Neg(x0), Pos(x1))
new_sr(Pos(x0), Neg(x1))
new_compare(x0, x1, app(ty_Maybe, x2))
new_compare(x0, x1, app(ty_[], x2))
new_primCmpNat1(Succ(x0), Succ(x1))
new_primPlusNat1(Zero, Zero)
new_merge1(x0, x1, [], x2)
new_compare(x0, x1, ty_Ordering)
new_merge2(:(x0, x1), :(x2, x3), x4)
new_primMulNat0(Succ(x0), Zero)
new_compare14(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_compare5(x0, x1)
new_primPlusNat1(Succ(x0), Zero)
new_compare(x0, x1, ty_Char)
new_primCmpNat1(Zero, Zero)
new_compare4(x0, x1, x2)
new_merge2(x0, [], x1)
new_sr(Pos(x0), Pos(x1))
new_compare14(x0, x1, ty_@0)
new_primPlusNat1(Zero, Succ(x0))
new_merge_pairs0(:(x0, []), x1)
new_merge2([], :(x0, x1), x2)
new_compare14(x0, x1, app(app(ty_@2, x2), x3))
new_primCmpNat1(Zero, Succ(x0))
new_compare1(x0, x1)
new_compare13(Pos(Zero), Pos(Succ(x0)))
new_compare14(x0, x1, ty_Char)
new_merge_pairs0([], x0)
new_compare13(Neg(Succ(x0)), Neg(x1))
new_merge1(x0, :(x1, x2), :(x3, x4), x5)
new_compare(x0, x1, app(app(ty_Either, x2), x3))
new_merge_pairs0(:(x0, :(x1, x2)), x3)
new_compare13(Pos(Zero), Neg(Zero))
new_compare13(Neg(Zero), Pos(Zero))
new_primCmpNat0(Succ(x0), x1)
new_compare14(x0, x1, ty_Float)
new_primPlusNat0(Zero, x0)
new_compare12(Float(x0, x1), Float(x2, x3))
new_compare10(x0, x1)
new_compare6(x0, x1)
new_compare(x0, x1, app(ty_Ratio, x2))
new_compare13(Neg(Zero), Neg(Succ(x0)))
new_primPlusNat0(Succ(x0), x1)
new_compare9(x0, x1)
new_compare14(x0, x1, ty_Int)
new_sr(Neg(x0), Neg(x1))
new_compare(x0, x1, ty_Int)
new_compare3(x0, x1)
new_primMulNat0(Succ(x0), Succ(x1))
new_compare13(Neg(Zero), Pos(Succ(x0)))
new_compare13(Pos(Zero), Neg(Succ(x0)))
new_compare(x0, x1, ty_Double)
new_compare14(x0, x1, ty_Double)
new_compare13(Pos(Succ(x0)), Pos(x1))
new_compare7(x0, x1, x2, x3)
new_compare13(Neg(Zero), Neg(Zero))
new_compare14(x0, x1, ty_Integer)
new_primMulNat0(Zero, Succ(x0))
new_compare(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_compare14(x0, x1, ty_Bool)
new_compare(x0, x1, ty_Float)
new_compare14(x0, x1, app(ty_Maybe, x2))
new_compare14(x0, x1, ty_Ordering)
new_compare(x0, x1, ty_Bool)
new_primPlusNat1(Succ(x0), Succ(x1))
new_compare0(x0, x1, x2)
new_compare13(Pos(Zero), Pos(Zero))
new_merge00(x0, x1, x2, x3, LT, x4)
new_merge00(x0, x1, x2, x3, EQ, x4)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ DependencyGraphProof

                      ↳ QDP

                        ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

new_mergesort'(vz514, :(vz5150, :(vz51510, vz51511)), ba) → new_mergesort'(new_merge1(vz514, vz5150, vz51510, ba), new_merge_pairs0(vz51511, ba), ba)

The TRS R consists of the following rules:

new_sr(Neg(vz517010), Neg(vz516010)) → Pos(new_primMulNat0(vz517010, vz516010))
new_compare7(vz5140, vz51500, bc, bd) → error([])
new_primCmpNat1(Succ(vz5140000), Succ(vz51500000)) → new_primCmpNat1(vz5140000, vz51500000)
new_primCmpNat0(Succ(vz5150000), vz514000) → new_primCmpNat1(vz5150000, vz514000)
new_compare10(vz5140, vz51500) → error([])
new_sr(Pos(vz517010), Pos(vz516010)) → Pos(new_primMulNat0(vz517010, vz516010))
new_merge00(vz524, vz525, vz526, vz527, LT, be) → :(vz525, new_merge2(vz526, :(vz524, vz527), be))
new_compare14(vz51500, vz515100, app(ty_Ratio, ca)) → new_compare8(vz51500, vz515100, ca)
new_compare(vz5140, vz51500, app(ty_Maybe, bb)) → new_compare0(vz5140, vz51500, bb)
new_primPlusNat1(Succ(vz52900), Succ(vz51601000)) → Succ(Succ(new_primPlusNat1(vz52900, vz51601000)))
new_merge_pairs0(:(vz515110, :(vz5151110, vz5151111)), ba) → :(new_merge2(vz515110, vz5151110, ba), new_merge_pairs0(vz5151111, ba))
new_compare14(vz51500, vz515100, app(app(app(ty_@3, cb), cc), cd)) → new_compare11(vz51500, vz515100, cb, cc, cd)
new_compare(vz5140, vz51500, ty_Int) → new_compare13(vz5140, vz51500)
new_merge1(vz514, [], :(vz515100, vz515101), ba) → new_merge2(vz514, :(vz515100, vz515101), ba)
new_merge_pairs0(:(vz515110, []), ba) → :(vz515110, [])
new_primMulNat0(Succ(vz5170100), Zero) → Zero
new_primMulNat0(Zero, Succ(vz5160100)) → Zero
new_compare13(Neg(Succ(vz514000)), Pos(vz515000)) → LT
new_compare(vz5140, vz51500, app(app(ty_@2, bf), bg)) → new_compare2(vz5140, vz51500, bf, bg)
new_compare2(vz5140, vz51500, bf, bg) → error([])
new_compare(vz5140, vz51500, app(ty_Ratio, ca)) → new_compare8(vz5140, vz51500, ca)
new_compare12(Float(vz51700, vz51701), Float(vz51600, vz51601)) → new_compare13(new_sr(vz51700, vz51600), new_sr(vz51701, vz51601))
new_compare(vz5140, vz51500, app(app(ty_Either, bc), bd)) → new_compare7(vz5140, vz51500, bc, bd)
new_compare(vz5140, vz51500, ty_Bool) → new_compare3(vz5140, vz51500)
new_primCmpNat2(vz514000, Zero) → GT
new_merge1(vz514, :(vz51500, vz51501), :(vz515100, vz515101), ba) → new_merge2(vz514, new_merge00(vz515100, vz51500, vz51501, vz515101, new_compare14(vz51500, vz515100, ba), ba), ba)
new_compare0(vz5140, vz51500, bb) → error([])
new_primPlusNat1(Zero, Zero) → Zero
new_compare(vz5140, vz51500, ty_Char) → new_compare9(vz5140, vz51500)
new_primCmpNat1(Zero, Succ(vz51500000)) → LT
new_compare13(Neg(Zero), Neg(Succ(vz5150000))) → new_primCmpNat2(vz5150000, Zero)
new_compare14(vz51500, vz515100, ty_Bool) → new_compare3(vz51500, vz515100)
new_merge00(vz524, vz525, vz526, vz527, GT, be) → :(vz524, new_merge2(:(vz525, vz526), vz527, be))
new_primMulNat0(Succ(vz5170100), Succ(vz5160100)) → new_primPlusNat0(new_primMulNat0(vz5170100, Succ(vz5160100)), vz5160100)
new_compare14(vz51500, vz515100, ty_Integer) → new_compare10(vz51500, vz515100)
new_compare9(vz5140, vz51500) → error([])
new_compare14(vz51500, vz515100, ty_Char) → new_compare9(vz51500, vz515100)
new_primCmpNat0(Zero, vz514000) → LT
new_compare3(vz5140, vz51500) → error([])
new_compare(vz5140, vz51500, ty_Integer) → new_compare10(vz5140, vz51500)
new_primCmpNat1(Zero, Zero) → EQ
new_compare4(vz5140, vz51500, bh) → error([])
new_merge2([], :(vz51500, vz51501), ba) → :(vz51500, vz51501)
new_compare(vz5140, vz51500, ty_Float) → new_compare12(vz5140, vz51500)
new_primMulNat0(Zero, Zero) → Zero
new_merge_pairs0([], ba) → []
new_compare14(vz51500, vz515100, app(ty_Maybe, bb)) → new_compare0(vz51500, vz515100, bb)
new_compare14(vz51500, vz515100, ty_Double) → new_compare6(vz51500, vz515100)
new_compare14(vz51500, vz515100, ty_Int) → new_compare13(vz51500, vz515100)
new_primPlusNat0(Succ(vz5290), vz5160100) → Succ(Succ(new_primPlusNat1(vz5290, vz5160100)))
new_compare14(vz51500, vz515100, app(ty_[], bh)) → new_compare4(vz51500, vz515100, bh)
new_compare(vz5140, vz51500, ty_Double) → new_compare6(vz5140, vz51500)
new_merge1(vz514, vz5150, [], ba) → new_merge2(vz514, vz5150, ba)
new_merge2(:(vz5140, vz5141), :(vz51500, vz51501), ba) → new_merge00(vz51500, vz5140, vz5141, vz51501, new_compare(vz5140, vz51500, ba), ba)
new_compare(vz5140, vz51500, app(ty_[], bh)) → new_compare4(vz5140, vz51500, bh)
new_compare14(vz51500, vz515100, ty_Float) → new_compare12(vz51500, vz515100)
new_compare14(vz51500, vz515100, ty_@0) → new_compare1(vz51500, vz515100)
new_compare14(vz51500, vz515100, app(app(ty_@2, bf), bg)) → new_compare2(vz51500, vz515100, bf, bg)
new_compare13(Pos(Zero), Pos(Succ(vz5150000))) → new_primCmpNat0(Zero, vz5150000)
new_primPlusNat0(Zero, vz5160100) → Succ(vz5160100)
new_compare11(vz5140, vz51500, cb, cc, cd) → error([])
new_merge2(vz514, [], ba) → vz514
new_compare13(Neg(Zero), Neg(Zero)) → EQ
new_primCmpNat1(Succ(vz5140000), Zero) → GT
new_compare14(vz51500, vz515100, app(app(ty_Either, bc), bd)) → new_compare7(vz51500, vz515100, bc, bd)
new_compare1(vz5140, vz51500) → error([])
new_compare(vz5140, vz51500, ty_@0) → new_compare1(vz5140, vz51500)
new_compare6(vz5140, vz51500) → error([])
new_compare13(Pos(Zero), Neg(Succ(vz5150000))) → GT
new_compare8(vz5140, vz51500, ca) → error([])
new_compare5(vz5140, vz51500) → error([])
new_compare13(Pos(Succ(vz514000)), Pos(vz515000)) → new_primCmpNat2(vz514000, vz515000)
new_compare(vz5140, vz51500, ty_Ordering) → new_compare5(vz5140, vz51500)
new_compare13(Pos(Zero), Neg(Zero)) → EQ
new_compare13(Neg(Zero), Pos(Zero)) → EQ
new_primPlusNat1(Succ(vz52900), Zero) → Succ(vz52900)
new_primPlusNat1(Zero, Succ(vz51601000)) → Succ(vz51601000)
new_compare13(Neg(Zero), Pos(Succ(vz5150000))) → LT
new_sr(Neg(vz517010), Pos(vz516010)) → Neg(new_primMulNat0(vz517010, vz516010))
new_sr(Pos(vz517010), Neg(vz516010)) → Neg(new_primMulNat0(vz517010, vz516010))
new_compare(vz5140, vz51500, app(app(app(ty_@3, cb), cc), cd)) → new_compare11(vz5140, vz51500, cb, cc, cd)
new_merge00(vz524, vz525, vz526, vz527, EQ, be) → :(vz525, new_merge2(vz526, :(vz524, vz527), be))
new_compare14(vz51500, vz515100, ty_Ordering) → new_compare5(vz51500, vz515100)
new_compare13(Pos(Zero), Pos(Zero)) → EQ
new_primCmpNat2(vz514000, Succ(vz5150000)) → new_primCmpNat1(vz514000, vz5150000)
new_compare13(Neg(Succ(vz514000)), Neg(vz515000)) → new_primCmpNat0(vz515000, vz514000)
new_compare13(Pos(Succ(vz514000)), Neg(vz515000)) → GT

The set Q consists of the following terms:

new_compare13(Pos(Succ(x0)), Neg(x1))
new_primCmpNat1(Succ(x0), Zero)
new_compare13(Neg(Succ(x0)), Pos(x1))
new_compare8(x0, x1, x2)
new_compare14(x0, x1, app(ty_Ratio, x2))
new_compare14(x0, x1, app(app(ty_Either, x2), x3))
new_compare2(x0, x1, x2, x3)
new_primCmpNat2(x0, Zero)
new_primCmpNat2(x0, Succ(x1))
new_compare14(x0, x1, app(ty_[], x2))
new_compare(x0, x1, app(app(ty_@2, x2), x3))
new_merge1(x0, [], :(x1, x2), x3)
new_primMulNat0(Zero, Zero)
new_compare(x0, x1, ty_@0)
new_compare(x0, x1, ty_Integer)
new_primCmpNat0(Zero, x0)
new_merge00(x0, x1, x2, x3, GT, x4)
new_compare11(x0, x1, x2, x3, x4)
new_sr(Neg(x0), Pos(x1))
new_sr(Pos(x0), Neg(x1))
new_compare(x0, x1, app(ty_Maybe, x2))
new_compare(x0, x1, app(ty_[], x2))
new_primCmpNat1(Succ(x0), Succ(x1))
new_primPlusNat1(Zero, Zero)
new_merge1(x0, x1, [], x2)
new_compare(x0, x1, ty_Ordering)
new_merge2(:(x0, x1), :(x2, x3), x4)
new_primMulNat0(Succ(x0), Zero)
new_compare14(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_compare5(x0, x1)
new_primPlusNat1(Succ(x0), Zero)
new_compare(x0, x1, ty_Char)
new_primCmpNat1(Zero, Zero)
new_compare4(x0, x1, x2)
new_merge2(x0, [], x1)
new_sr(Pos(x0), Pos(x1))
new_compare14(x0, x1, ty_@0)
new_primPlusNat1(Zero, Succ(x0))
new_merge_pairs0(:(x0, []), x1)
new_merge2([], :(x0, x1), x2)
new_compare14(x0, x1, app(app(ty_@2, x2), x3))
new_primCmpNat1(Zero, Succ(x0))
new_compare1(x0, x1)
new_compare13(Pos(Zero), Pos(Succ(x0)))
new_compare14(x0, x1, ty_Char)
new_merge_pairs0([], x0)
new_compare13(Neg(Succ(x0)), Neg(x1))
new_merge1(x0, :(x1, x2), :(x3, x4), x5)
new_compare(x0, x1, app(app(ty_Either, x2), x3))
new_merge_pairs0(:(x0, :(x1, x2)), x3)
new_compare13(Pos(Zero), Neg(Zero))
new_compare13(Neg(Zero), Pos(Zero))
new_primCmpNat0(Succ(x0), x1)
new_compare14(x0, x1, ty_Float)
new_primPlusNat0(Zero, x0)
new_compare12(Float(x0, x1), Float(x2, x3))
new_compare10(x0, x1)
new_compare6(x0, x1)
new_compare(x0, x1, app(ty_Ratio, x2))
new_compare13(Neg(Zero), Neg(Succ(x0)))
new_primPlusNat0(Succ(x0), x1)
new_compare9(x0, x1)
new_compare14(x0, x1, ty_Int)
new_sr(Neg(x0), Neg(x1))
new_compare(x0, x1, ty_Int)
new_compare3(x0, x1)
new_primMulNat0(Succ(x0), Succ(x1))
new_compare13(Neg(Zero), Pos(Succ(x0)))
new_compare13(Pos(Zero), Neg(Succ(x0)))
new_compare(x0, x1, ty_Double)
new_compare14(x0, x1, ty_Double)
new_compare13(Pos(Succ(x0)), Pos(x1))
new_compare7(x0, x1, x2, x3)
new_compare13(Neg(Zero), Neg(Zero))
new_compare14(x0, x1, ty_Integer)
new_primMulNat0(Zero, Succ(x0))
new_compare(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_compare14(x0, x1, ty_Bool)
new_compare(x0, x1, ty_Float)
new_compare14(x0, x1, app(ty_Maybe, x2))
new_compare14(x0, x1, ty_Ordering)
new_compare(x0, x1, ty_Bool)
new_primPlusNat1(Succ(x0), Succ(x1))
new_compare0(x0, x1, x2)
new_compare13(Pos(Zero), Pos(Zero))
new_merge00(x0, x1, x2, x3, LT, x4)
new_merge00(x0, x1, x2, x3, EQ, x4)

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

new_mergesort'(vz514, :(vz5150, :(vz51510, vz51511)), ba) → new_mergesort'(new_merge1(vz514, vz5150, vz51510, ba), new_merge_pairs0(vz51511, ba), ba)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [25]:

POL(:(x₁, x₂)) = 1 + x₂
POL(EQ) = 0
POL(Float(x₁, x₂)) = x₁ + x₂
POL(GT) = 0
POL(LT) = 0
POL(Neg(x₁)) = x₁
POL(Pos(x₁)) = x₁
POL(Succ(x₁)) = 1
POL(Zero) = 0
POL([]) = 0
POL(app(x₁, x₂)) = x₂
POL(error(x₁)) = 0
POL(new_compare(x₁, x₂, x₃)) = 1 + x₁ + x₃
POL(new_compare0(x₁, x₂, x₃)) = 0
POL(new_compare1(x₁, x₂)) = 0
POL(new_compare10(x₁, x₂)) = 0
POL(new_compare11(x₁, x₂, x₃, x₄, x₅)) = 0
POL(new_compare12(x₁, x₂)) = 1 + x₁
POL(new_compare13(x₁, x₂)) = 1 + x₁
POL(new_compare14(x₁, x₂, x₃)) = 0
POL(new_compare2(x₁, x₂, x₃, x₄)) = 0
POL(new_compare3(x₁, x₂)) = 1
POL(new_compare4(x₁, x₂, x₃)) = 1
POL(new_compare5(x₁, x₂)) = 0
POL(new_compare6(x₁, x₂)) = 1
POL(new_compare7(x₁, x₂, x₃, x₄)) = 0
POL(new_compare8(x₁, x₂, x₃)) = 1
POL(new_compare9(x₁, x₂)) = 1
POL(new_merge00(x₁, x₂, x₃, x₄, x₅, x₆)) = 0
POL(new_merge1(x₁, x₂, x₃, x₄)) = 0
POL(new_merge2(x₁, x₂, x₃)) = 0
POL(new_merge_pairs0(x₁, x₂)) = x₁
POL(new_mergesort'(x₁, x₂, x₃)) = x₂
POL(new_primCmpNat0(x₁, x₂)) = 1
POL(new_primCmpNat1(x₁, x₂)) = 1
POL(new_primCmpNat2(x₁, x₂)) = 1
POL(new_primMulNat0(x₁, x₂)) = 0
POL(new_primPlusNat0(x₁, x₂)) = 0
POL(new_primPlusNat1(x₁, x₂)) = 0
POL(new_sr(x₁, x₂)) = x₁
POL(ty_@0) = 0
POL(ty_@2) = 0
POL(ty_@3) = 0
POL(ty_Bool) = 1
POL(ty_Char) = 1
POL(ty_Double) = 1
POL(ty_Either) = 0
POL(ty_Float) = 1
POL(ty_Int) = 1
POL(ty_Integer) = 0
POL(ty_Maybe) = 0
POL(ty_Ordering) = 0
POL(ty_Ratio) = 0
POL(ty_[]) = 0

The following usable rules [17] were oriented:

new_merge_pairs0([], ba) → []
new_merge_pairs0(:(vz515110, :(vz5151110, vz5151111)), ba) → :(new_merge2(vz515110, vz5151110, ba), new_merge_pairs0(vz5151111, ba))
new_merge_pairs0(:(vz515110, []), ba) → :(vz515110, [])

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ DependencyGraphProof

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ PisEmptyProof

Q DP problem:
P is empty.
The TRS R consists of the following rules:

new_sr(Neg(vz517010), Neg(vz516010)) → Pos(new_primMulNat0(vz517010, vz516010))
new_compare7(vz5140, vz51500, bc, bd) → error([])
new_primCmpNat1(Succ(vz5140000), Succ(vz51500000)) → new_primCmpNat1(vz5140000, vz51500000)
new_primCmpNat0(Succ(vz5150000), vz514000) → new_primCmpNat1(vz5150000, vz514000)
new_compare10(vz5140, vz51500) → error([])
new_sr(Pos(vz517010), Pos(vz516010)) → Pos(new_primMulNat0(vz517010, vz516010))
new_merge00(vz524, vz525, vz526, vz527, LT, be) → :(vz525, new_merge2(vz526, :(vz524, vz527), be))
new_compare14(vz51500, vz515100, app(ty_Ratio, ca)) → new_compare8(vz51500, vz515100, ca)
new_compare(vz5140, vz51500, app(ty_Maybe, bb)) → new_compare0(vz5140, vz51500, bb)
new_primPlusNat1(Succ(vz52900), Succ(vz51601000)) → Succ(Succ(new_primPlusNat1(vz52900, vz51601000)))
new_merge_pairs0(:(vz515110, :(vz5151110, vz5151111)), ba) → :(new_merge2(vz515110, vz5151110, ba), new_merge_pairs0(vz5151111, ba))
new_compare14(vz51500, vz515100, app(app(app(ty_@3, cb), cc), cd)) → new_compare11(vz51500, vz515100, cb, cc, cd)
new_compare(vz5140, vz51500, ty_Int) → new_compare13(vz5140, vz51500)
new_merge1(vz514, [], :(vz515100, vz515101), ba) → new_merge2(vz514, :(vz515100, vz515101), ba)
new_merge_pairs0(:(vz515110, []), ba) → :(vz515110, [])
new_primMulNat0(Succ(vz5170100), Zero) → Zero
new_primMulNat0(Zero, Succ(vz5160100)) → Zero
new_compare13(Neg(Succ(vz514000)), Pos(vz515000)) → LT
new_compare(vz5140, vz51500, app(app(ty_@2, bf), bg)) → new_compare2(vz5140, vz51500, bf, bg)
new_compare2(vz5140, vz51500, bf, bg) → error([])
new_compare(vz5140, vz51500, app(ty_Ratio, ca)) → new_compare8(vz5140, vz51500, ca)
new_compare12(Float(vz51700, vz51701), Float(vz51600, vz51601)) → new_compare13(new_sr(vz51700, vz51600), new_sr(vz51701, vz51601))
new_compare(vz5140, vz51500, app(app(ty_Either, bc), bd)) → new_compare7(vz5140, vz51500, bc, bd)
new_compare(vz5140, vz51500, ty_Bool) → new_compare3(vz5140, vz51500)
new_primCmpNat2(vz514000, Zero) → GT
new_merge1(vz514, :(vz51500, vz51501), :(vz515100, vz515101), ba) → new_merge2(vz514, new_merge00(vz515100, vz51500, vz51501, vz515101, new_compare14(vz51500, vz515100, ba), ba), ba)
new_compare0(vz5140, vz51500, bb) → error([])
new_primPlusNat1(Zero, Zero) → Zero
new_compare(vz5140, vz51500, ty_Char) → new_compare9(vz5140, vz51500)
new_primCmpNat1(Zero, Succ(vz51500000)) → LT
new_compare13(Neg(Zero), Neg(Succ(vz5150000))) → new_primCmpNat2(vz5150000, Zero)
new_compare14(vz51500, vz515100, ty_Bool) → new_compare3(vz51500, vz515100)
new_merge00(vz524, vz525, vz526, vz527, GT, be) → :(vz524, new_merge2(:(vz525, vz526), vz527, be))
new_primMulNat0(Succ(vz5170100), Succ(vz5160100)) → new_primPlusNat0(new_primMulNat0(vz5170100, Succ(vz5160100)), vz5160100)
new_compare14(vz51500, vz515100, ty_Integer) → new_compare10(vz51500, vz515100)
new_compare9(vz5140, vz51500) → error([])
new_compare14(vz51500, vz515100, ty_Char) → new_compare9(vz51500, vz515100)
new_primCmpNat0(Zero, vz514000) → LT
new_compare3(vz5140, vz51500) → error([])
new_compare(vz5140, vz51500, ty_Integer) → new_compare10(vz5140, vz51500)
new_primCmpNat1(Zero, Zero) → EQ
new_compare4(vz5140, vz51500, bh) → error([])
new_merge2([], :(vz51500, vz51501), ba) → :(vz51500, vz51501)
new_compare(vz5140, vz51500, ty_Float) → new_compare12(vz5140, vz51500)
new_primMulNat0(Zero, Zero) → Zero
new_merge_pairs0([], ba) → []
new_compare14(vz51500, vz515100, app(ty_Maybe, bb)) → new_compare0(vz51500, vz515100, bb)
new_compare14(vz51500, vz515100, ty_Double) → new_compare6(vz51500, vz515100)
new_compare14(vz51500, vz515100, ty_Int) → new_compare13(vz51500, vz515100)
new_primPlusNat0(Succ(vz5290), vz5160100) → Succ(Succ(new_primPlusNat1(vz5290, vz5160100)))
new_compare14(vz51500, vz515100, app(ty_[], bh)) → new_compare4(vz51500, vz515100, bh)
new_compare(vz5140, vz51500, ty_Double) → new_compare6(vz5140, vz51500)
new_merge1(vz514, vz5150, [], ba) → new_merge2(vz514, vz5150, ba)
new_merge2(:(vz5140, vz5141), :(vz51500, vz51501), ba) → new_merge00(vz51500, vz5140, vz5141, vz51501, new_compare(vz5140, vz51500, ba), ba)
new_compare(vz5140, vz51500, app(ty_[], bh)) → new_compare4(vz5140, vz51500, bh)
new_compare14(vz51500, vz515100, ty_Float) → new_compare12(vz51500, vz515100)
new_compare14(vz51500, vz515100, ty_@0) → new_compare1(vz51500, vz515100)
new_compare14(vz51500, vz515100, app(app(ty_@2, bf), bg)) → new_compare2(vz51500, vz515100, bf, bg)
new_compare13(Pos(Zero), Pos(Succ(vz5150000))) → new_primCmpNat0(Zero, vz5150000)
new_primPlusNat0(Zero, vz5160100) → Succ(vz5160100)
new_compare11(vz5140, vz51500, cb, cc, cd) → error([])
new_merge2(vz514, [], ba) → vz514
new_compare13(Neg(Zero), Neg(Zero)) → EQ
new_primCmpNat1(Succ(vz5140000), Zero) → GT
new_compare14(vz51500, vz515100, app(app(ty_Either, bc), bd)) → new_compare7(vz51500, vz515100, bc, bd)
new_compare1(vz5140, vz51500) → error([])
new_compare(vz5140, vz51500, ty_@0) → new_compare1(vz5140, vz51500)
new_compare6(vz5140, vz51500) → error([])
new_compare13(Pos(Zero), Neg(Succ(vz5150000))) → GT
new_compare8(vz5140, vz51500, ca) → error([])
new_compare5(vz5140, vz51500) → error([])
new_compare13(Pos(Succ(vz514000)), Pos(vz515000)) → new_primCmpNat2(vz514000, vz515000)
new_compare(vz5140, vz51500, ty_Ordering) → new_compare5(vz5140, vz51500)
new_compare13(Pos(Zero), Neg(Zero)) → EQ
new_compare13(Neg(Zero), Pos(Zero)) → EQ
new_primPlusNat1(Succ(vz52900), Zero) → Succ(vz52900)
new_primPlusNat1(Zero, Succ(vz51601000)) → Succ(vz51601000)
new_compare13(Neg(Zero), Pos(Succ(vz5150000))) → LT
new_sr(Neg(vz517010), Pos(vz516010)) → Neg(new_primMulNat0(vz517010, vz516010))
new_sr(Pos(vz517010), Neg(vz516010)) → Neg(new_primMulNat0(vz517010, vz516010))
new_compare(vz5140, vz51500, app(app(app(ty_@3, cb), cc), cd)) → new_compare11(vz5140, vz51500, cb, cc, cd)
new_merge00(vz524, vz525, vz526, vz527, EQ, be) → :(vz525, new_merge2(vz526, :(vz524, vz527), be))
new_compare14(vz51500, vz515100, ty_Ordering) → new_compare5(vz51500, vz515100)
new_compare13(Pos(Zero), Pos(Zero)) → EQ
new_primCmpNat2(vz514000, Succ(vz5150000)) → new_primCmpNat1(vz514000, vz5150000)
new_compare13(Neg(Succ(vz514000)), Neg(vz515000)) → new_primCmpNat0(vz515000, vz514000)
new_compare13(Pos(Succ(vz514000)), Neg(vz515000)) → GT

The set Q consists of the following terms:

new_compare13(Pos(Succ(x0)), Neg(x1))
new_primCmpNat1(Succ(x0), Zero)
new_compare13(Neg(Succ(x0)), Pos(x1))
new_compare8(x0, x1, x2)
new_compare14(x0, x1, app(ty_Ratio, x2))
new_compare14(x0, x1, app(app(ty_Either, x2), x3))
new_compare2(x0, x1, x2, x3)
new_primCmpNat2(x0, Zero)
new_primCmpNat2(x0, Succ(x1))
new_compare14(x0, x1, app(ty_[], x2))
new_compare(x0, x1, app(app(ty_@2, x2), x3))
new_merge1(x0, [], :(x1, x2), x3)
new_primMulNat0(Zero, Zero)
new_compare(x0, x1, ty_@0)
new_compare(x0, x1, ty_Integer)
new_primCmpNat0(Zero, x0)
new_merge00(x0, x1, x2, x3, GT, x4)
new_compare11(x0, x1, x2, x3, x4)
new_sr(Neg(x0), Pos(x1))
new_sr(Pos(x0), Neg(x1))
new_compare(x0, x1, app(ty_Maybe, x2))
new_compare(x0, x1, app(ty_[], x2))
new_primCmpNat1(Succ(x0), Succ(x1))
new_primPlusNat1(Zero, Zero)
new_merge1(x0, x1, [], x2)
new_compare(x0, x1, ty_Ordering)
new_merge2(:(x0, x1), :(x2, x3), x4)
new_primMulNat0(Succ(x0), Zero)
new_compare14(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_compare5(x0, x1)
new_primPlusNat1(Succ(x0), Zero)
new_compare(x0, x1, ty_Char)
new_primCmpNat1(Zero, Zero)
new_compare4(x0, x1, x2)
new_merge2(x0, [], x1)
new_sr(Pos(x0), Pos(x1))
new_compare14(x0, x1, ty_@0)
new_primPlusNat1(Zero, Succ(x0))
new_merge_pairs0(:(x0, []), x1)
new_merge2([], :(x0, x1), x2)
new_compare14(x0, x1, app(app(ty_@2, x2), x3))
new_primCmpNat1(Zero, Succ(x0))
new_compare1(x0, x1)
new_compare13(Pos(Zero), Pos(Succ(x0)))
new_compare14(x0, x1, ty_Char)
new_merge_pairs0([], x0)
new_compare13(Neg(Succ(x0)), Neg(x1))
new_merge1(x0, :(x1, x2), :(x3, x4), x5)
new_compare(x0, x1, app(app(ty_Either, x2), x3))
new_merge_pairs0(:(x0, :(x1, x2)), x3)
new_compare13(Pos(Zero), Neg(Zero))
new_compare13(Neg(Zero), Pos(Zero))
new_primCmpNat0(Succ(x0), x1)
new_compare14(x0, x1, ty_Float)
new_primPlusNat0(Zero, x0)
new_compare12(Float(x0, x1), Float(x2, x3))
new_compare10(x0, x1)
new_compare6(x0, x1)
new_compare(x0, x1, app(ty_Ratio, x2))
new_compare13(Neg(Zero), Neg(Succ(x0)))
new_primPlusNat0(Succ(x0), x1)
new_compare9(x0, x1)
new_compare14(x0, x1, ty_Int)
new_sr(Neg(x0), Neg(x1))
new_compare(x0, x1, ty_Int)
new_compare3(x0, x1)
new_primMulNat0(Succ(x0), Succ(x1))
new_compare13(Neg(Zero), Pos(Succ(x0)))
new_compare13(Pos(Zero), Neg(Succ(x0)))
new_compare(x0, x1, ty_Double)
new_compare14(x0, x1, ty_Double)
new_compare13(Pos(Succ(x0)), Pos(x1))
new_compare7(x0, x1, x2, x3)
new_compare13(Neg(Zero), Neg(Zero))
new_compare14(x0, x1, ty_Integer)
new_primMulNat0(Zero, Succ(x0))
new_compare(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_compare14(x0, x1, ty_Bool)
new_compare(x0, x1, ty_Float)
new_compare14(x0, x1, app(ty_Maybe, x2))
new_compare14(x0, x1, ty_Ordering)
new_compare(x0, x1, ty_Bool)
new_primPlusNat1(Succ(x0), Succ(x1))
new_compare0(x0, x1, x2)
new_compare13(Pos(Zero), Pos(Zero))
new_merge00(x0, x1, x2, x3, LT, x4)
new_merge00(x0, x1, x2, x3, EQ, x4)

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

case	cmp x y of
	GT	→ y : merge cmp (x : xs) ys
	_	→ x : merge cmp xs (y : ys)

merge0	y cmp x xs ys GT	= y : merge cmp (x : xs) ys
merge0	y cmp x xs ys _	= x : merge cmp xs (y : ys)